diff options
| author | emakarov | 2007-11-03 19:20:51 +0000 |
|---|---|---|
| committer | emakarov | 2007-11-03 19:20:51 +0000 |
| commit | e38fc39f64d8af81fc237889329953bfafa29422 (patch) | |
| tree | da8c6f96671bb1d387b9267827b300e153250675 /theories/Numbers/Natural/Binary | |
| parent | 4e6e719d23b9cfc0e9d21cce065c795c1037bccb (diff) | |
An update of theories/Numbers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10285 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural/Binary')
| -rw-r--r-- | theories/Numbers/Natural/Binary/NBinary.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index b35af2e01a..abd98ebefd 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -137,11 +137,11 @@ Qed. Theorem recursion_wd : forall (A : Set) (Aeq : relation A), forall a a' : A, Aeq a a' -> - forall f f' : N -> A -> A, eq_fun2 NZeq Aeq Aeq f f' -> + forall f f' : N -> A -> A, fun2_eq NZeq Aeq Aeq f f' -> forall x x' : N, x = x' -> Aeq (recursion a f x) (recursion a' f' x'). Proof. -unfold fun2_wd, NZeq, eq_fun2. +unfold fun2_wd, NZeq, fun2_eq. intros A Aeq a a' Eaa' f f' Eff'. intro x; pattern x; apply Nind. intros x' H; now rewrite <- H. |