nlemma proj1: ∀A,B:Prop.A ∧ B → A.
#A; #B; #H;
- napply (And_ind A B ?? H);
+ napply (And_ind A B … H);
#H1; #H2;
napply H1.
nqed.
nlemma proj2: ∀A,B:Prop.A ∧ B → B.
#A; #B; #H;
- napply (And_ind A B ?? H);
+ napply (And_ind A B … H);
#H1; #H2;
napply H2.
nqed.
nnormalize;
#x; #y; #H;
nrewrite < H;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
#A; #x; #P; #H; #y; #H1;
- nrewrite < (symmetric_eq ??? H1);
+ nrewrite < (symmetric_eq … H1);
napply H.
nqed.
nchange with (match cons T x2 y2 with [ nil ⇒ False | cons a _ ⇒ x1 = a ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma list_destruct_2 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → y1 = y2.
nchange with (match cons T x2 y2 with [ nil ⇒ False | cons _ b ⇒ y1 = b ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma list_destruct_cons_nil : ∀T.∀x:T.∀y:list T.cons T x y = nil T → False.
#T; #l;
nelim l;
nnormalize;
- ##[ ##1: napply (refl_eq ??)
+ ##[ ##1: napply refl_eq
##| ##2: #x; #y; #H;
nrewrite > H;
- napply (refl_eq ??)
+ napply refl_eq
##]
nqed.
#T; #x; #y; #z;
nelim x;
nnormalize;
- ##[ ##1: napply (refl_eq ??)
+ ##[ ##1: napply refl_eq
##| ##2: #a; #b; #H;
nrewrite > H;
- napply (refl_eq ??)
+ napply refl_eq
##]
nqed.
nlemma cons_append_commute : ∀T:Type.∀l1,l2:list T.∀a:T.a :: (l1 @ l2) = (a :: l1) @ l2.
#T; #l1; #l2; #a;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma append_cons_commute : ∀T:Type.∀a:T.∀l,l1:list T.l @ (a::l1) = (l@[a]) @ l1.
#T; #a; #l; #l1;
nrewrite > (associative_list T l [a] l1);
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.