diff options
Diffstat (limited to 'theories/Sets/Finite_sets.v')
| -rwxr-xr-x | theories/Sets/Finite_sets.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v index 1e0c05450..1e7168791 100755 --- a/theories/Sets/Finite_sets.v +++ b/theories/Sets/Finite_sets.v @@ -59,8 +59,8 @@ Lemma cardinal_invert : [n:nat] (EXT A | (EXT x | X == (Add U A x) /\ ~ (In U A x) /\ (cardinal U A n))) end. Proof. -Induction 1; Simpl; Auto. -Intros; Exists A; Exists x; Auto. +NewInduction 1; Simpl; Auto. +Exists A; Exists x; Auto. Qed. Lemma cardinal_elim : |