diff options
Diffstat (limited to 'theories/Init/Wf.v')
| -rwxr-xr-x | theories/Init/Wf.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 745af5ef6..4fb640827 100755 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -107,7 +107,7 @@ Apply F_ext; Auto. Qed. -Lemma fix_eq : (x:A)(fix x)=(F x [y:A][p:(R y x)](fix y)). +Lemma Fix_eq : (x:A)(fix x)=(F x [y:A][p:(R y x)](fix y)). Intro; Unfold fix. Case (Fix_F_eq x). Apply F_ext; Intros. |