Commit c349ec80 authored by Robbert Krebbers's avatar Robbert Krebbers

Add a Notation for `sn`: strongly normalizing.

parent 03966a39
......@@ -54,6 +54,9 @@ Section definitions.
| ex_loop_do_step x y : R x y ex_loop y ex_loop x.
End definitions.
(* Strongly normalizing elements *)
Notation sn R := (Acc (flip R)).
Hint Unfold nf red.
(** * General theorems *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment