diff options
| author | Jasper Hugunin | 2020-08-22 15:55:17 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-25 13:53:31 -0700 |
| commit | d6b1274515890c22930ae54ff0b7bb492eebd622 (patch) | |
| tree | b73c4c6069621f651af241e1f0839c630569e86c /theories/Init | |
| parent | 560b2888ffb414ae711b6158b5506ed79d6e039d (diff) | |
Modify Init/Wf.v to compile with -mangle-names
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Wf.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index a305626eb3..60200ae0f6 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -85,8 +85,7 @@ Section Well_founded. Scheme Acc_inv_dep := Induction for Acc Sort Prop. - Lemma Fix_F_eq : - forall (x:A) (r:Acc x), + Lemma Fix_F_eq (x:A) (r:Acc x) : F (fun (y:A) (p:R y x) => Fix_F (x:=y) (Acc_inv r p)) = Fix_F (x:=x) r. Proof. destruct r using Acc_inv_dep; auto. @@ -104,7 +103,7 @@ Section Well_founded. Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F r = Fix_F s. Proof. - intro x; induction (Rwf x); intros. + intro x; induction (Rwf x); intros r s. rewrite <- (Fix_F_eq r); rewrite <- (Fix_F_eq s); intros. apply F_ext; auto. Qed. |