nchange with (match pair T1 T2 x2 y2 with [ pair a _ ⇒ x1 = a ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma pair_destruct_2 :
nchange with (match pair T1 T2 x2 y2 with [ pair _ b ⇒ y1 = b ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma symmetric_eqpair :
nrewrite > (H x1 x2);
ncases (f1 x2 x1);
nnormalize;
- ##[ ##1: nrewrite > (H1 y1 y2); napply (refl_eq ??)
- ##| ##2: napply (refl_eq ??)
+ ##[ ##1: nrewrite > (H1 y1 y2); napply refl_eq
+ ##| ##2: napply refl_eq
##]
nqed.
nelim p2;
#x2; #y2; #H;
nnormalize;
- nrewrite > (H1 ?? (pair_destruct_1 ?????? H));
+ nrewrite > (H1 … (pair_destruct_1 … H));
nnormalize;
- nrewrite > (H2 ?? (pair_destruct_2 ?????? H));
- napply (refl_eq ??).
+ nrewrite > (H2 … (pair_destruct_2 … H));
+ napply refl_eq.
nqed.
nlemma eqpair_to_eq :
ncases (f1 x1 x2) in H:(%) K:(%);
nnormalize;
#H3;
- ##[ ##2: napply (bool_destruct ??? H3) ##]
+ ##[ ##2: napply (bool_destruct … H3) ##]
#H4;
- nrewrite > (H4 (refl_eq ??));
+ nrewrite > (H4 (refl_eq …));
nrewrite > (H2 y1 y2 H3);
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma triple_destruct_1 :
nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple a _ _ ⇒ x1 = a ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma triple_destruct_2 :
nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ b _ ⇒ y1 = b ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma triple_destruct_3 :
nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ _ c ⇒ z1 = c ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma symmetric_eqtriple :
##[ ##1: nrewrite > (H1 y1 y2);
ncases (f2 y2 y1);
nnormalize;
- ##[ ##1: nrewrite > (H2 z1 z2); napply (refl_eq ??)
- ##| ##2: napply (refl_eq ??)
+ ##[ ##1: nrewrite > (H2 z1 z2); napply refl_eq
+ ##| ##2: napply refl_eq
##]
- ##| ##2: napply (refl_eq ??)
+ ##| ##2: napply refl_eq
##]
nqed.
nelim p2;
#x2; #y2; #z2; #H;
nnormalize;
- nrewrite > (H1 ?? (triple_destruct_1 ????????? H));
+ nrewrite > (H1 … (triple_destruct_1 … H));
nnormalize;
- nrewrite > (H2 ?? (triple_destruct_2 ????????? H));
+ nrewrite > (H2 … (triple_destruct_2 … H));
nnormalize;
- nrewrite > (H3 ?? (triple_destruct_3 ????????? H));
- napply (refl_eq ??).
+ nrewrite > (H3 … (triple_destruct_3 … H));
+ napply refl_eq.
nqed.
nlemma eqtriple_to_eq :
nletin K ≝ (H1 x1 x2);
ncases (f1 x1 x2) in H:(%) K:(%);
nnormalize;
- ##[ ##2: #H4; napply (bool_destruct ??? H4) ##]
+ ##[ ##2: #H4; napply (bool_destruct … H4) ##]
nletin K1 ≝ (H2 y1 y2);
ncases (f2 y1 y2) in K1:(%) ⊢ %;
nnormalize;
- ##[ ##2: #H4; #H5; napply (bool_destruct ??? H5) ##]
+ ##[ ##2: #H4; #H5; napply (bool_destruct … H5) ##]
#H4; #H5; #H6;
- nrewrite > (H4 (refl_eq ??));
- nrewrite > (H6 (refl_eq ??));
+ nrewrite > (H4 (refl_eq …));
+ nrewrite > (H6 (refl_eq …));
nrewrite > (H3 z1 z2 H5);
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma quadruple_destruct_1 :
nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple a _ _ _ ⇒ x1 = a ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma quadruple_destruct_2 :
nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ b _ _ ⇒ y1 = b ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma quadruple_destruct_3 :
nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ c _ ⇒ z1 = c ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma quadruple_destruct_4 :
nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ _ d ⇒ v1 = d ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma symmetric_eqquadruple :
##[ ##1: nrewrite > (H2 z1 z2);
ncases (f3 z2 z1);
nnormalize;
- ##[ ##1: nrewrite > (H3 v1 v2); napply (refl_eq ??)
- ##| ##2: napply (refl_eq ??)
+ ##[ ##1: nrewrite > (H3 v1 v2); napply refl_eq
+ ##| ##2: napply refl_eq
##]
- ##| ##2: napply (refl_eq ??)
+ ##| ##2: napply refl_eq
##]
- ##| ##2: napply (refl_eq ??)
+ ##| ##2: napply refl_eq
##]
nqed.
nelim p2;
#x2; #y2; #z2; #v2; #H;
nnormalize;
- nrewrite > (H1 ?? (quadruple_destruct_1 ???????????? H));
+ nrewrite > (H1 … (quadruple_destruct_1 … H));
nnormalize;
- nrewrite > (H2 ?? (quadruple_destruct_2 ???????????? H));
+ nrewrite > (H2 … (quadruple_destruct_2 … H));
nnormalize;
- nrewrite > (H3 ?? (quadruple_destruct_3 ???????????? H));
+ nrewrite > (H3 … (quadruple_destruct_3 … H));
nnormalize;
- nrewrite > (H4 ?? (quadruple_destruct_4 ???????????? H));
- napply (refl_eq ??).
+ nrewrite > (H4 … (quadruple_destruct_4 … H));
+ napply refl_eq.
nqed.
nlemma eqquadruple_to_eq :
nletin K ≝ (H1 x1 x2);
ncases (f1 x1 x2) in H:(%) K:(%);
nnormalize;
- ##[ ##2: #H5; napply (bool_destruct ??? H5) ##]
+ ##[ ##2: #H5; napply (bool_destruct … H5) ##]
nletin K1 ≝ (H2 y1 y2);
ncases (f2 y1 y2) in K1:(%) ⊢ %;
nnormalize;
- ##[ ##2: #H5; #H6; napply (bool_destruct ??? H6) ##]
+ ##[ ##2: #H5; #H6; napply (bool_destruct … H6) ##]
nletin K2 ≝ (H3 z1 z2);
ncases (f3 z1 z2) in K2:(%) ⊢ %;
nnormalize;
- ##[ ##2: #H5; #H6; #H7; napply (bool_destruct ??? H7) ##]
+ ##[ ##2: #H5; #H6; #H7; napply (bool_destruct … H7) ##]
#H5; #H6; #H7; #H8;
- nrewrite > (H5 (refl_eq ??));
- nrewrite > (H6 (refl_eq ??));
- nrewrite > (H8 (refl_eq ??));
+ nrewrite > (H5 (refl_eq …));
+ nrewrite > (H6 (refl_eq …));
+ nrewrite > (H8 (refl_eq …));
nrewrite > (H4 v1 v2 H7);
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma quintuple_destruct_1 :
nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple a _ _ _ _ ⇒ x1 = a ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma quintuple_destruct_2 :
nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ b _ _ _ ⇒ y1 = b ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma quintuple_destruct_3 :
nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ c _ _ ⇒ z1 = c ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma quintuple_destruct_4 :
nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ d _ ⇒ v1 = d ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma quintuple_destruct_5 :
nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ _ e ⇒ w1 = e ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma symmetric_eqquintuple :
##[ ##1: nrewrite > (H3 v1 v2);
ncases (f4 v2 v1);
nnormalize;
- ##[ ##1: nrewrite > (H4 w1 w2); napply (refl_eq ??)
- ##| ##2: napply (refl_eq ??)
+ ##[ ##1: nrewrite > (H4 w1 w2); napply refl_eq
+ ##| ##2: napply refl_eq
##]
- ##| ##2: napply (refl_eq ??)
+ ##| ##2: napply refl_eq
##]
- ##| ##2: napply (refl_eq ??)
+ ##| ##2: napply refl_eq
##]
- ##| ##2: napply (refl_eq ??)
+ ##| ##2: napply refl_eq
##]
nqed.
nelim p2;
#x2; #y2; #z2; #v2; #w2; #H;
nnormalize;
- nrewrite > (H1 ?? (quintuple_destruct_1 ??????????????? H));
+ nrewrite > (H1 … (quintuple_destruct_1 … H));
nnormalize;
- nrewrite > (H2 ?? (quintuple_destruct_2 ??????????????? H));
+ nrewrite > (H2 … (quintuple_destruct_2 … H));
nnormalize;
- nrewrite > (H3 ?? (quintuple_destruct_3 ??????????????? H));
+ nrewrite > (H3 … (quintuple_destruct_3 … H));
nnormalize;
- nrewrite > (H4 ?? (quintuple_destruct_4 ??????????????? H));
+ nrewrite > (H4 … (quintuple_destruct_4 … H));
nnormalize;
- nrewrite > (H5 ?? (quintuple_destruct_5 ??????????????? H));
- napply (refl_eq ??).
+ nrewrite > (H5 … (quintuple_destruct_5 … H));
+ napply refl_eq.
nqed.
nlemma eqquintuple_to_eq :
nletin K ≝ (H1 x1 x2);
ncases (f1 x1 x2) in H:(%) K:(%);
nnormalize;
- ##[ ##2: #H6; napply (bool_destruct ??? H6) ##]
+ ##[ ##2: #H6; napply (bool_destruct … H6) ##]
nletin K1 ≝ (H2 y1 y2);
ncases (f2 y1 y2) in K1:(%) ⊢ %;
nnormalize;
- ##[ ##2: #H6; #H7; napply (bool_destruct ??? H7) ##]
+ ##[ ##2: #H6; #H7; napply (bool_destruct … H7) ##]
nletin K2 ≝ (H3 z1 z2);
ncases (f3 z1 z2) in K2:(%) ⊢ %;
nnormalize;
- ##[ ##2: #H6; #H7; #H8; napply (bool_destruct ??? H8) ##]
+ ##[ ##2: #H6; #H7; #H8; napply (bool_destruct … H8) ##]
nletin K3 ≝ (H4 v1 v2);
ncases (f4 v1 v2) in K3:(%) ⊢ %;
nnormalize;
- ##[ ##2: #H6; #H7; #H8; #H9; napply (bool_destruct ??? H9) ##]
+ ##[ ##2: #H6; #H7; #H8; #H9; napply (bool_destruct … H9) ##]
#H6; #H7; #H8; #H9; #H10;
- nrewrite > (H6 (refl_eq ??));
- nrewrite > (H7 (refl_eq ??));
- nrewrite > (H8 (refl_eq ??));
- nrewrite > (H10 (refl_eq ??));
+ nrewrite > (H6 (refl_eq …));
+ nrewrite > (H7 (refl_eq …));
+ nrewrite > (H8 (refl_eq …));
+ nrewrite > (H10 (refl_eq …));
nrewrite > (H5 w1 w2 H9);
- napply (refl_eq ??).
+ napply refl_eq.
nqed.