diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract/NStrongRec.v')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NStrongRec.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index 67cab5507..f98e8da9a 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -13,7 +13,7 @@ and proves its properties *) Require Export NSub. -Ltac f_equiv' := repeat (f_equiv; try intros ? ? ?; auto). +Ltac f_equiv' := repeat (repeat f_equiv; try intros ? ? ?; auto). Module NStrongRecProp (Import N : NAxiomsRecSig'). Include NSubProp N. @@ -82,7 +82,6 @@ Proof. intros. unfold strong_rec0. f_equiv. rewrite recursion_succ; f_equiv'. -reflexivity. Qed. Lemma strong_rec_0 : forall a, |