diff options
| -rwxr-xr-x | theories/Init/Wf.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 3d4d0efba..5a05f7b65 100755 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -29,8 +29,8 @@ Section Well_founded. (** The accessibility predicate is defined to be non-informative *) - Inductive Acc (a: A) : Prop := - Acc_intro : (forall y:A, R y a -> Acc y) -> Acc a. + Inductive Acc (x: A) : Prop := + Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x. Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y. destruct 1; trivial. |