Commit 4d688329 authored by Robbert Krebbers's avatar Robbert Krebbers

Simplify Fix_F_proper.

parent d19ceda8
......@@ -222,9 +222,7 @@ computation (that is, we cannot make it opaque). We use the [Strategy]
command to make its expanding behavior less eager. *)
Strategy 100 [wf_guard].
Lemma Fix_F_proper `{R : relation A}
(B : A Type)
(E : x, relation (B x)) {E_Equivalence : x, Equivalence (E x)}
Lemma Fix_F_proper `{R : relation A} (B : A Type) (E : x, relation (B x))
(F : x, ( y, R y x B y) B x)
(HF : (x : A) (f g : y, R y x B y),
( y Hy Hy', E _ (f y Hy) (g y Hy')) E _ (F x f) (F x g))
......
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