nelim b2;
#e3; #e4;
nchange with (
- match plus_ex_dc_dc e2 e4 c with
- [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with
- [ pair h c' ⇒ pair … 〈h,l〉 c' ]] =
- match plus_ex_dc_dc e4 e2 c with
- [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with
- [ pair h c' ⇒ pair … 〈h,l〉 c' ]]);
+ match plus_ex_dc_dc e2 e4 c with [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with [ pair h c' ⇒ pair … 〈h,l〉 c' ]] =
+ match plus_ex_dc_dc e4 e2 c with [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with [ pair h c' ⇒ pair … 〈h,l〉 c' ]]);
nrewrite > (symmetric_plusex_dc_dc e4 e2 c);
ncases (plus_ex_dc_dc e2 e4 c);
#e5; #c1;
nchange with (
- match plus_ex_dc_dc e1 e3 c1 with
- [ pair h c' ⇒ pair … 〈h,e5〉 c' ] =
- match plus_ex_dc_dc e3 e1 c1 with
- [ pair h c' ⇒ pair … 〈h,e5〉 c' ]);
+ match plus_ex_dc_dc e1 e3 c1 with [ pair h c' ⇒ pair … 〈h,e5〉 c' ] =
+ match plus_ex_dc_dc e3 e1 c1 with [ pair h c' ⇒ pair … 〈h,e5〉 c' ]);
nrewrite > (symmetric_plusex_dc_dc e1 e3 c1);
napply refl_eq.
nqed.
nelim b2;
#e3; #e4;
nchange with (
- match plus_ex_dc_dc e2 e4 c with
- [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
- match plus_ex_dc_dc e4 e2 c with
- [ pair l c ⇒ 〈plus_ex_dc_d e3 e1 c,l〉 ]);
+ match plus_ex_dc_dc e2 e4 c with [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
+ match plus_ex_dc_dc e4 e2 c with [ pair l c ⇒ 〈plus_ex_dc_d e3 e1 c,l〉 ]);
nrewrite > (symmetric_plusex_dc_dc e4 e2 c);
ncases (plus_ex_dc_dc e2 e4 c);
#e5; #c1;
nelim b2;
#e3; #e4;
nchange with (
- match plus_ex_d_dc e2 e4 with
- [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with
- [ pair h c' ⇒ pair … 〈h,l〉 c' ]] =
- match plus_ex_d_dc e4 e2 with
- [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with
- [ pair h c' ⇒ pair … 〈h,l〉 c' ]]);
+ match plus_ex_d_dc e2 e4 with [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with [ pair h c' ⇒ pair … 〈h,l〉 c' ]] =
+ match plus_ex_d_dc e4 e2 with [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with [ pair h c' ⇒ pair … 〈h,l〉 c' ]]);
nrewrite > (symmetric_plusex_d_dc e4 e2);
ncases (plus_ex_d_dc e2 e4);
#e5; #c;
nchange with (
- match plus_ex_dc_dc e1 e3 c with
- [ pair h c' ⇒ pair … 〈h,e5〉 c' ] =
- match plus_ex_dc_dc e3 e1 c with
- [ pair h c' ⇒ pair … 〈h,e5〉 c' ]);
+ match plus_ex_dc_dc e1 e3 c with [ pair h c' ⇒ pair … 〈h,e5〉 c' ] =
+ match plus_ex_dc_dc e3 e1 c with [ pair h c' ⇒ pair … 〈h,e5〉 c' ]);
nrewrite > (symmetric_plusex_dc_dc e1 e3 c);
napply refl_eq.
nqed.
nelim b2;
#e3; #e4;
nchange with (
- match plus_ex_d_dc e2 e4 with
- [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
- match plus_ex_d_dc e4 e2 with
- [ pair l c ⇒ 〈plus_ex_dc_d e3 e1 c,l〉 ]);
+ match plus_ex_d_dc e2 e4 with [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
+ match plus_ex_d_dc e4 e2 with [ pair l c ⇒ 〈plus_ex_dc_d e3 e1 c,l〉 ]);
nrewrite > (symmetric_plusex_d_dc e4 e2);
ncases (plus_ex_d_dc e2 e4);
#e5; #c;
#e1; #e2; #e3; #e4;
nchange with ((((eq_ex e3 e1) ⊗ (eq_ex e4 e2)) = false) → ?);
#H;
- napply (or2_elim ((eq_ex e3 e1) = false) ((eq_ex e4 e2) = false) ? (andb_false … H) …);
+ napply (or2_elim ((eq_ex e3 e1) = false) ((eq_ex e4 e2) = false) ? (andb_false2 … H) …);
##[ ##1: #H1; napply (decidable_b8_aux1 … (neqex_to_neq … H1))
##| ##2: #H1; napply (decidable_b8_aux2 … (neqex_to_neq … H1))
##]