Commit 1d45f474 authored by Robbert Krebbers's avatar Robbert Krebbers

Monotonicity for `Acc`.

parent 7b4dc84f
......@@ -315,6 +315,10 @@ Section subrel.
End subrel.
(** * Theorems on well founded relations *)
Lemma Acc_impl {A} (R1 R2 : relation A) x :
Acc R1 x ( y1 y2, R2 y1 y2 R1 y1 y2) Acc R2 x.
Proof. induction 1; constructor; naive_solver. Qed.
Notation wf := well_founded.
Definition wf_guard `{R : relation A} (n : nat) (wfR : wf R) : wf R :=
Acc_intro_generator n wfR.
......
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