14
Theorem zero_leq_three: 0 <= 3.
27
Lemma zero_leq_three': 0 <= 3.
32
Lemma zero_lt_three : 0 < 3.
47
Check (nil (A:= nat -> nat)).
49
Check (fun A: Set => (cons (A:=A))).
51
Check (cons 3 (cons 2 nil)).
56
Require Import Bvector.
62
Check (fun (A:Set)(a:A)=> Vcons _ a _ (Vnil _)).
64
Check (Vcons _ 5 _ (Vcons _ 3 _ (Vnil _))).
78
Lemma eq_3_3 : 2 + 1 = 3.
84
Lemma eq_proof_proof : refl_equal (2*6) = refl_equal (3*4).
90
Lemma eq_lt_le : ( 2 < 4) = (3 <= 4).
95
Lemma eq_nat_nat : nat = nat.
100
Lemma eq_Set_Set : Set = Set.
105
Lemma eq_Type_Type : Type = Type.
130
Require Import ZArith.
131
Require Import Compare_dec.
135
Definition max (n p :nat) := match le_lt_dec n p with
140
Theorem le_max : forall n p, n <= p -> max n p = p.
142
intros n p ; unfold max ; case (le_lt_dec n p); simpl.
144
intros; absurd (p < p); eauto with arith.
154
Inductive tree(A:Set) : Set :=
155
node : A -> forest A -> tree A
157
forest (A: Set) : Set :=
159
addchild : tree A -> forest A -> forest A.
168
evenS : forall n, odd n -> even (S n)
171
oddS : forall n, even n -> odd (S n).
173
Lemma odd_49 : odd (7 * 7).
174
simpl; repeat constructor.
179
Definition nat_case :=
180
fun (Q : Type)(g0 : Q)(g1 : nat -> Q)(n:nat) =>
181
match n return Q with
186
Eval simpl in (nat_case nat 0 (fun p => p) 34).
188
Eval simpl in (fun g0 g1 => nat_case nat g0 g1 34).
190
Eval simpl in (fun g0 g1 => nat_case nat g0 g1 0).
193
Definition pred (n:nat) := match n with O => O | S m => m end.
195
Eval simpl in pred 56.
197
Eval simpl in pred 0.
199
Eval simpl in fun p => pred (S p).
202
Definition xorb (b1 b2:bool) :=
204
| false, true => true
205
| true, false => true
210
Definition pred_spec (n:nat) := {m:nat | n=0 /\ m=0 \/ n = S m}.
213
Definition predecessor : forall n:nat, pred_spec n.
215
unfold pred_spec;exists 0;auto.
216
unfold pred_spec; intro n0;exists n0; auto.
221
Extraction predecessor.
224
forall n:nat, n = match n with 0 => 0 | S p => S p end.
225
intro n;case n;simpl;auto.
228
Check (fun p:False => match p return 2=3 with end).
230
Theorem fromFalse : False -> 0=1.
235
Section equality_elimination.
240
Check (fun H : Q a =>
241
match p in (eq _ y) return Q y with
245
End equality_elimination.
248
Theorem trans : forall n m p:nat, n=m -> m=p -> n=p.
255
Lemma Rw : forall x y: nat, y = y * x -> y * x * x = y.
256
intros x y e; do 2 rewrite <- e.
261
Require Import Arith.
266
: forall n : nat, 1 * n = n
269
Check mult_plus_distr_r.
272
: forall n m p : nat, (n + m) * p = n * p + m * p
276
Lemma mult_distr_S : forall n p : nat, n * p + p = (S n)* p.
277
simpl;auto with arith.
280
Lemma four_n : forall n:nat, n+n+n+n = 4*n.
281
intro n;rewrite <- (mult_1_l n).
284
intro n; pattern n at 1.
288
repeat rewrite mult_distr_S.
293
Section Le_case_analysis.
294
Variables (n p : nat)
298
(HS : forall m, n <= m -> Q (S m)).
300
match H in (_ <= q) return (Q q) with
302
| le_S m Hm => HS m Hm
307
End Le_case_analysis.
310
Lemma predecessor_of_positive : forall n, 1 <= n -> exists p:nat, n = S p.
314
intros m Hm; exists m;trivial.
317
Definition Vtail_total
318
(A : Set) (n : nat) (v : vector A n) : vector A (pred n):=
319
match v in (vector _ n0) return (vector A (pred n0)) with
321
| Vcons _ n0 v0 => v0
324
Definition Vtail' (A:Set)(n:nat)(v:vector A n) : vector A (pred n).
325
intros A n v; case v.
333
Inductive Lambda : Set :=
334
lambda : (Lambda -> False) -> Lambda.
337
Error: Non strictly positive occurrence of "Lambda" in
338
"(Lambda -> False) -> Lambda"
343
Variable Lambda : Set.
344
Variable lambda : (Lambda -> False) ->Lambda.
346
Variable matchL : Lambda -> forall Q:Prop, ((Lambda ->False) -> Q) -> Q.
348
understand matchL Q l (fun h : Lambda -> False => t)
350
as match l return Q with lambda h => t end
353
Definition application (f x: Lambda) :False :=
354
matchL f False (fun h => h x).
356
Definition Delta : Lambda := lambda (fun x : Lambda => application x x).
358
Definition loop : False := application Delta Delta.
360
Theorem two_is_three : 2 = 3.
368
Require Import ZArith.
372
Inductive itree : Set :=
374
| inode : Z-> (nat -> itree) -> itree.
376
Definition isingle l := inode l (fun i => ileaf).
378
Definition t1 := inode 0 (fun n => isingle (Z_of_nat (2*n))).
380
Definition t2 := inode 0
383
(fun p => isingle (Z_of_nat (n*p)))).
386
Inductive itree_le : itree-> itree -> Prop :=
387
| le_leaf : forall t, itree_le ileaf t
388
| le_node : forall l l' s s',
390
(forall i, exists j:nat, itree_le (s i) (s' j)) ->
391
itree_le (inode l s) (inode l' s').
394
Theorem itree_le_trans :
395
forall t t', itree_le t t' ->
396
forall t'', itree_le t' t'' -> itree_le t t''.
408
inversion_clear H0;eauto with zarith.
410
intro i2; case (H4 i2).
412
generalize (H i2 _ H0).
415
generalize (H5 _ H6).
421
Inductive itree_le' : itree-> itree -> Prop :=
422
| le_leaf' : forall t, itree_le' ileaf t
423
| le_node' : forall l l' s s' g,
425
(forall i, itree_le' (s i) (s' (g i))) ->
426
itree_le' (inode l s) (inode l' s').
432
Lemma t1_le_t2 : itree_le t1 t2.
436
intro i; exists (2 * i).
440
exists i;constructor.
445
Lemma t1_le'_t2 : itree_le' t1 t2.
447
constructor 2 with (fun i : nat => 2 * i).
450
intro i ; constructor 2 with (fun i :nat => i).
458
Inductive ltree (A:Set) : Set :=
459
lnode : A -> list (ltree A) -> ltree A.
461
Inductive prop : Prop :=
462
prop_intro : Prop -> prop.
464
Lemma prop_inject: prop.
465
Proof prop_intro prop.
468
Inductive ex_Prop (P : Prop -> Prop) : Prop :=
469
exP_intro : forall X : Prop, P X -> ex_Prop P.
471
Lemma ex_Prop_inhabitant : ex_Prop (fun P => P -> P).
473
exists (ex_Prop (fun P => P -> P)).
482
Check (fun (P:Prop->Prop)(p: ex_Prop P) =>
483
match p with exP_intro X HX => X end).
485
Incorrect elimination of "p" in the inductive type
486
"ex_Prop", the return type has sort "Type" while it should be
489
Elimination of an inductive object of sort "Prop"
490
is not allowed on a predicate in sort "Type"
491
because proofs can be eliminated only to build proofs
496
Check (match prop_inject with (prop_intro P p) => P end).
499
Incorrect elimination of "prop_inject" in the inductive type
500
"prop", the return type has sort "Type" while it should be
503
Elimination of an inductive object of sort "Prop"
504
is not allowed on a predicate in sort "Type"
505
because proofs can be eliminated only to build proofs
512
prop_inject = prop_intro prop (fun H : prop => H)
517
Inductive typ : Type :=
518
typ_intro : Type -> typ.
520
Definition typ_inject: typ.
526
Error: Universe Inconsistency.
531
Inductive aSet : Set :=
532
aSet_intro: Set -> aSet.
535
User error: Large non-propositional inductive types must be in Type
539
Inductive ex_Set (P : Set -> Prop) : Type :=
540
exS_intro : forall X : Set, P X -> ex_Set P.
543
Inductive comes_from_the_left (P Q:Prop): P \/ Q -> Prop :=
544
c1 : forall p, comes_from_the_left P Q (or_introl (A:=P) Q p).
546
Goal (comes_from_the_left _ _ (or_introl True I)).
550
Goal ~(comes_from_the_left _ _ (or_intror True I)).
556
Reset comes_from_the_left.
565
Definition comes_from_the_left (P Q:Prop)(H:P \/ Q): Prop :=
567
| or_introl p => True
568
| or_intror q => False
572
Incorrect elimination of "H" in the inductive type
573
"or", the return type has sort "Type" while it should be
576
Elimination of an inductive object of sort "Prop"
577
is not allowed on a predicate in sort "Type"
578
because proofs can be eliminated only to build proofs
582
Definition comes_from_the_left_sumbool
583
(P Q:Prop)(x:{P}+{Q}): Prop :=
598
Theorem S_is_not_O : forall n, S n <> 0.
600
Definition Is_zero (x:nat):= match x with
604
Lemma O_is_zero : forall m, m = 0 -> Is_zero m.
608
============================
615
apply O_is_zero with (m := S n).
619
Theorem disc2 : forall n, S (S n) <> 1.
621
intros n Hn; discriminate.
625
Theorem disc3 : forall n, S (S n) = 0 -> forall Q:Prop, Q.
633
Theorem inj_succ : forall n m, S n = S m -> n = m.
637
Lemma inj_pred : forall n m, n = m -> pred n = pred m.
645
apply inj_pred with (n:= S n) (m := S m); assumption.
648
Lemma list_inject : forall (A:Set)(a b :A)(l l':list A),
649
a :: b :: l = b :: a :: l' -> a = b /\ l = l'.
657
Theorem not_le_Sn_0 : forall n:nat, ~ (S n <= 0).
663
Lemma not_le_Sn_0_with_constraints :
664
forall n p , S n <= p -> p = 0 -> False.
666
intros n p H; case H ;
667
intros; discriminate.
670
eapply not_le_Sn_0_with_constraints; eauto.
674
Theorem not_le_Sn_0' : forall n:nat, ~ (S n <= 0).
676
red; intros n H ; inversion H.
679
Derive Inversion le_Sn_0_inv with (forall n :nat, S n <= 0).
682
Theorem le_Sn_0'' : forall n p : nat, ~ S n <= 0 .
685
inversion H using le_Sn_0_inv.
688
Derive Inversion_clear le_Sn_0_inv' with (forall n :nat, S n <= 0).
692
Theorem le_reverse_rules :
693
forall n m:nat, n <= m ->
695
exists p, n <= p /\ m = S p.
697
intros n m H; inversion H.
699
right; exists m0; split; trivial.
701
intros n m H; inversion_clear H.
703
right; exists m0; split; trivial.
706
Inductive ArithExp : Set :=
708
| Succ : ArithExp -> ArithExp
709
| Plus : ArithExp -> ArithExp -> ArithExp.
711
Inductive RewriteRel : ArithExp -> ArithExp -> Prop :=
712
RewSucc : forall e1 e2 :ArithExp,
713
RewriteRel e1 e2 -> RewriteRel (Succ e1) (Succ e2)
714
| RewPlus0 : forall e:ArithExp,
715
RewriteRel (Plus Zero e) e
716
| RewPlusS : forall e1 e2:ArithExp,
718
RewriteRel (Plus (Succ e1) e2) (Succ (Plus e1 e2)).
722
Fixpoint plus (n p:nat) {struct n} : nat :=
725
| S m => S (plus m p)
728
Fixpoint plus' (n p:nat) {struct p} : nat :=
731
| S q => S (plus' n q)
734
Fixpoint plus'' (n p:nat) {struct n} : nat :=
737
| S m => plus'' m (S p)
741
Fixpoint even_test (n:nat) : bool :=
745
| S (S p) => even_test p
751
Fixpoint even_test (n:nat) : bool :=
757
with odd_test (n:nat) : bool :=
766
Eval simpl in even_test.
770
Eval simpl in (fun x : nat => even_test x).
772
Eval simpl in (fun x : nat => plus 5 x).
773
Eval simpl in (fun x : nat => even_test (plus 5 x)).
775
Eval simpl in (fun x : nat => even_test (plus x 5)).
778
Section Principle_of_Induction.
779
Variable P : nat -> Prop.
780
Hypothesis base_case : P 0.
781
Hypothesis inductive_step : forall n:nat, P n -> P (S n).
782
Fixpoint nat_ind (n:nat) : (P n) :=
783
match n return P n with
785
| S m => inductive_step m (nat_ind m)
788
End Principle_of_Induction.
790
Scheme Even_induction := Minimality for even Sort Prop
791
with Odd_induction := Minimality for odd Sort Prop.
793
Theorem even_plus_four : forall n:nat, even n -> even (4+n).
796
elim H using Even_induction with (P0 := fun n => odd (4+n));
797
simpl;repeat constructor;assumption.
801
Section Principle_of_Double_Induction.
802
Variable P : nat -> nat ->Prop.
803
Hypothesis base_case1 : forall x:nat, P 0 x.
804
Hypothesis base_case2 : forall x:nat, P (S x) 0.
805
Hypothesis inductive_step : forall n m:nat, P n m -> P (S n) (S m).
806
Fixpoint nat_double_ind (n m:nat){struct n} : P n m :=
807
match n, m return P n m with
808
| 0 , x => base_case1 x
809
| (S x), 0 => base_case2 x
810
| (S x), (S y) => inductive_step x y (nat_double_ind x y)
812
End Principle_of_Double_Induction.
814
Section Principle_of_Double_Recursion.
815
Variable P : nat -> nat -> Set.
816
Hypothesis base_case1 : forall x:nat, P 0 x.
817
Hypothesis base_case2 : forall x:nat, P (S x) 0.
818
Hypothesis inductive_step : forall n m:nat, P n m -> P (S n) (S m).
819
Fixpoint nat_double_rec (n m:nat){struct n} : P n m :=
820
match n, m return P n m with
821
| 0 , x => base_case1 x
822
| (S x), 0 => base_case2 x
823
| (S x), (S y) => inductive_step x y (nat_double_rec x y)
825
End Principle_of_Double_Recursion.
827
Definition min : nat -> nat -> nat :=
828
nat_double_rec (fun (x y:nat) => nat)
831
(fun (x y r:nat) => S r).
833
Eval compute in (min 5 8).
834
Eval compute in (min 8 5).
838
Lemma not_circular : forall n:nat, n <> S n.
841
apply nat_ind with (P:= fun n => n <> S n).
843
red; intros n0 Hn0 eqn0Sn0;injection eqn0Sn0;trivial.
846
Definition eq_nat_dec : forall n p:nat , {n=p}+{n <> p}.
849
apply nat_double_rec with (P:= fun (n q:nat) => {q=p}+{q <> p}).
852
elim n using nat_double_rec.
855
intros n0 m H; case H.
856
intro eq; rewrite eq ; auto.
857
intro neg; right; red ; injection 1; auto.
860
Definition eq_nat_dec' : forall n p:nat, {n=p}+{n <> p}.
867
Require Import Minus.
870
Fixpoint div (x y:nat){struct x}: nat :=
873
else if eq_nat_dec y 0
875
else S (div (x-y) y).
878
Recursive definition of div is ill-formed.
880
div : nat -> nat -> nat
886
Recursive call to div has principal argument equal to
888
instead of a subterm of x
892
Lemma minus_smaller_S: forall x y:nat, x - y < S x.
894
intros x y; pattern y, x;
895
elim x using nat_double_ind.
896
destruct x0; auto with arith.
897
simpl; auto with arith.
898
simpl; auto with arith.
901
Lemma minus_smaller_positive : forall x y:nat, x <>0 -> y <> 0 ->
904
destruct x; destruct y;
905
( simpl;intros; apply minus_smaller_S ||
906
intros; absurd (0=0); auto).
909
Definition minus_decrease : forall x y:nat, Acc lt x ->
914
intros x y H; case H.
916
apply Hz; apply minus_smaller_positive; assumption.
919
Print minus_decrease.
923
Definition div_aux (x y:nat)(H: Acc lt x):nat.
926
refine (if eq_nat_dec x 0
928
else if eq_nat_dec y 0
930
else div_aux (x-y) y _).
931
apply (minus_decrease x y H);assumption.
938
(fix div_aux (x y : nat) (H : Acc lt x) {struct H} : nat :=
939
match eq_nat_dec x 0 with
942
match eq_nat_dec y 0 with
944
| right _0 => div_aux (x - y) y (minus_decrease x y H _ _0)
947
: forall x : nat, nat -> Acc lt x -> nat
950
Require Import Wf_nat.
951
Definition div x y := div_aux x y (lt_wf x).
962
let rec div_aux x y =
963
match eq_nat_dec x O with
966
(match eq_nat_dec y O with
968
| Right -> div_aux (minus x y) y)
971
Lemma vector0_is_vnil : forall (A:Set)(v:vector A 0), v = Vnil A.
973
intros A v;inversion v.
977
Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n),
980
Toplevel input, characters 40281-40287
981
> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n), n= 0 -> v = Vnil A.
983
Error: In environment
988
The term "Vnil A" has type "vector A 0" while it is expected to have type
993
Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n),
994
n= 0 -> JMeq v (Vnil A).
1001
Lemma vector0_is_vnil : forall (A:Set)(v:vector A 0), v = Vnil A.
1003
intros a v;apply JMeq_eq.
1004
apply vector0_is_vnil_aux.
1009
Implicit Arguments Vcons [A n].
1010
Implicit Arguments Vnil [A].
1011
Implicit Arguments Vhead [A n].
1012
Implicit Arguments Vtail [A n].
1014
Definition Vid : forall (A : Type)(n:nat), vector A n -> vector A n.
1016
destruct n; intro v.
1018
exact (Vcons (Vhead v) (Vtail v)).
1021
Eval simpl in (fun (A:Set)(v:vector A 0) => (Vid _ _ v)).
1023
Eval simpl in (fun (A:Set)(v:vector A 0) => v).
1027
Lemma Vid_eq : forall (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v).
1034
Theorem zero_nil : forall A (v:vector A 0), v = Vnil.
1037
change (Vnil (A:=A)) with (Vid _ 0 v).
1043
forall (A : Set) (n : nat) (v : vector A (S n)),
1044
v = Vcons (Vhead v) (Vtail v).
1047
change (Vcons (Vhead v) (Vtail v)) with (Vid _ (S n) v).
1053
Definition vector_double_rect :
1054
forall (A:Set) (P: forall (n:nat),(vector A n)->(vector A n) -> Type),
1056
(forall n (v1 v2 : vector A n) a b, P n v1 v2 ->
1057
P (S n) (Vcons a v1) (Vcons b v2)) ->
1058
forall n (v1 v2 : vector A n), P n v1 v2.
1060
intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2).
1062
intros v1 v2; rewrite (decomp _ _ v1);rewrite (decomp _ _ v2).
1066
Require Import Bool.
1068
Definition bitwise_or n v1 v2 : vector bool n :=
1069
vector_double_rect bool (fun n v1 v2 => vector bool n)
1071
(fun n v1 v2 a b r => Vcons (orb a b) r) n v1 v2.
1074
Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:vector A p){struct v}
1078
| 0 , Vcons b _ _ => Some b
1079
| S n', Vcons _ p' v' => vector_nth A n' p' v'
1082
Implicit Arguments vector_nth [A p].
1085
Lemma nth_bitwise : forall (n:nat) (v1 v2: vector bool n) i a b,
1086
vector_nth i v1 = Some a ->
1087
vector_nth i v2 = Some b ->
1088
vector_nth i (bitwise_or _ v1 v2) = Some (orb a b).
1090
intros n v1 v2; pattern n,v1,v2.
1091
apply vector_double_rect.
1093
destruct i; discriminate 1.
1094
destruct i; simpl;auto.
1095
injection 1; injection 2;intros; subst a; subst b; auto.
1098
Set Implicit Arguments.
1100
CoInductive Stream (A:Set) : Set :=
1101
| Cons : A -> Stream A -> Stream A.
1103
CoInductive LList (A: Set) : Set :=
1105
| LCons : A -> LList A -> LList A.
1111
Definition head (A:Set)(s : Stream A) := match s with Cons a s' => a end.
1113
Definition tail (A : Set)(s : Stream A) :=
1114
match s with Cons a s' => s' end.
1116
CoFixpoint repeat (A:Set)(a:A) : Stream A := Cons a (repeat a).
1118
CoFixpoint iterate (A: Set)(f: A -> A)(a : A) : Stream A:=
1119
Cons a (iterate f (f a)).
1121
CoFixpoint map (A B:Set)(f: A -> B)(s : Stream A) : Stream B:=
1122
match s with Cons a tl => Cons (f a) (map f tl) end.
1124
Eval simpl in (fun (A:Set)(a:A) => repeat a).
1126
Eval simpl in (fun (A:Set)(a:A) => head (repeat a)).
1129
CoInductive EqSt (A: Set) : Stream A -> Stream A -> Prop :=
1130
eqst : forall s1 s2: Stream A,
1131
head s1 = head s2 ->
1132
EqSt (tail s1) (tail s2) ->
1136
Section Parks_Principle.
1138
Variable R : Stream A -> Stream A -> Prop.
1139
Hypothesis bisim1 : forall s1 s2:Stream A, R s1 s2 ->
1141
Hypothesis bisim2 : forall s1 s2:Stream A, R s1 s2 ->
1142
R (tail s1) (tail s2).
1144
CoFixpoint park_ppl : forall s1 s2:Stream A, R s1 s2 ->
1146
fun s1 s2 (p : R s1 s2) =>
1147
eqst s1 s2 (bisim1 p)
1148
(park_ppl (bisim2 p)).
1149
End Parks_Principle.
1152
Theorem map_iterate : forall (A:Set)(f:A->A)(x:A),
1153
EqSt (iterate f (f x)) (map f (iterate f x)).
1157
(R:= fun s1 s2 => exists x: A,
1158
s1 = iterate f (f x) /\ s2 = map f (iterate f x)).
1160
intros s1 s2 (x0,(eqs1,eqs2));rewrite eqs1;rewrite eqs2;reflexivity.
1161
intros s1 s2 (x0,(eqs1,eqs2)).
1162
exists (f x0);split;[rewrite eqs1|rewrite eqs2]; reflexivity.
1163
exists x;split; reflexivity.
1166
Ltac infiniteproof f :=
1167
cofix f; constructor; [clear f| simpl; try (apply f; clear f)].
1170
Theorem map_iterate' : forall (A:Set)(f:A->A)(x:A),
1171
EqSt (iterate f (f x)) (map f (iterate f x)).
1172
infiniteproof map_iterate'.
1177
Implicit Arguments LNil [A].
1179
Lemma Lnil_not_Lcons : forall (A:Set)(a:A)(l:LList A),
1180
LNil <> (LCons a l).
1181
intros;discriminate.
1184
Lemma injection_demo : forall (A:Set)(a b : A)(l l': LList A),
1185
LCons a (LCons b l) = LCons b (LCons a l') ->
1188
intros A a b l l' e; injection e; auto.
1192
Inductive Finite (A:Set) : LList A -> Prop :=
1193
| Lnil_fin : Finite (LNil (A:=A))
1194
| Lcons_fin : forall a l, Finite l -> Finite (LCons a l).
1196
CoInductive Infinite (A:Set) : LList A -> Prop :=
1197
| LCons_inf : forall a l, Infinite l -> Infinite (LCons a l).
1199
Lemma LNil_not_Infinite : forall (A:Set), ~ Infinite (LNil (A:=A)).
1201
intros A H;inversion H.
1204
Lemma Finite_not_Infinite : forall (A:Set)(l:LList A),
1205
Finite l -> ~ Infinite l.
1207
intros A l H; elim H.
1208
apply LNil_not_Infinite.
1209
intros a l0 F0 I0' I1.
1210
case I0'; inversion_clear I1.
1214
Lemma Not_Finite_Infinite : forall (A:Set)(l:LList A),
1215
~ Finite l -> Infinite l.
1219
intro; absurd (Finite (LNil (A:=A)));[auto|constructor].
1222
red; intro H1;case H0.
added
removed
test-suite/success/RecTutorial.v
