nelim w2;
#b3; #b4;
nchange with (
- match plus_b8_dc_dc b2 b4 c with
- [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with
- [ pair h c' ⇒ pair … 〈h:l〉 c' ]] =
- match plus_b8_dc_dc b4 b2 c with
- [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with
- [ pair h c' ⇒ pair … 〈h:l〉 c' ]]);
+ match plus_b8_dc_dc b2 b4 c with [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with [ pair h c' ⇒ pair … 〈h:l〉 c' ]] =
+ match plus_b8_dc_dc b4 b2 c with [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with [ pair h c' ⇒ pair … 〈h:l〉 c' ]]);
nrewrite > (symmetric_plusb8_dc_dc b4 b2 c);
ncases (plus_b8_dc_dc b2 b4 c);
#b5; #c1;
nchange with (
- match plus_b8_dc_dc b1 b3 c1 with
- [ pair h c' ⇒ pair … 〈h:b5〉 c' ] =
- match plus_b8_dc_dc b3 b1 c1 with
- [ pair h c' ⇒ pair … 〈h:b5〉 c' ]);
+ match plus_b8_dc_dc b1 b3 c1 with [ pair h c' ⇒ pair … 〈h:b5〉 c' ] =
+ match plus_b8_dc_dc b3 b1 c1 with [ pair h c' ⇒ pair … 〈h:b5〉 c' ]);
nrewrite > (symmetric_plusb8_dc_dc b1 b3 c1);
napply refl_eq.
nqed.
nelim w2;
#b3; #b4;
nchange with (
- match plus_b8_dc_dc b2 b4 c with
- [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
- match plus_b8_dc_dc b4 b2 c with
- [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
+ match plus_b8_dc_dc b2 b4 c with [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
+ match plus_b8_dc_dc b4 b2 c with [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
nrewrite > (symmetric_plusb8_dc_dc b4 b2 c);
ncases (plus_b8_dc_dc b2 b4 c);
#b5; #c1;
nelim w2;
#b3; #b4;
nchange with (
- match plus_b8_d_dc b2 b4 with
- [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with
- [ pair h c' ⇒ pair … 〈h:l〉 c' ]] =
- match plus_b8_d_dc b4 b2 with
- [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with
- [ pair h c' ⇒ pair … 〈h:l〉 c' ]]);
+ match plus_b8_d_dc b2 b4 with [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with [ pair h c' ⇒ pair … 〈h:l〉 c' ]] =
+ match plus_b8_d_dc b4 b2 with [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with [ pair h c' ⇒ pair … 〈h:l〉 c' ]]);
nrewrite > (symmetric_plusb8_d_dc b4 b2);
ncases (plus_b8_d_dc b2 b4);
#b5; #c;
nchange with (
- match plus_b8_dc_dc b1 b3 c with
- [ pair h c' ⇒ pair … 〈h:b5〉 c' ] =
- match plus_b8_dc_dc b3 b1 c with
- [ pair h c' ⇒ pair … 〈h:b5〉 c' ]);
+ match plus_b8_dc_dc b1 b3 c with [ pair h c' ⇒ pair … 〈h:b5〉 c' ] =
+ match plus_b8_dc_dc b3 b1 c with [ pair h c' ⇒ pair … 〈h:b5〉 c' ]);
nrewrite > (symmetric_plusb8_dc_dc b1 b3 c);
napply refl_eq.
nqed.
nelim w2;
#b3; #b4;
nchange with (
- match plus_b8_d_dc b2 b4 with
- [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
- match plus_b8_d_dc b4 b2 with
- [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
+ match plus_b8_d_dc b2 b4 with [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
+ match plus_b8_d_dc b4 b2 with [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
nrewrite > (symmetric_plusb8_d_dc b4 b2);
ncases (plus_b8_d_dc b2 b4);
#b5; #c;
#b1; #b2; #b3; #b4;
nchange with ((((eq_b8 b3 b1) ⊗ (eq_b8 b4 b2)) = false) → ?);
#H;
- napply (or2_elim ((eq_b8 b3 b1) = false) ((eq_b8 b4 b2) = false) ? (andb_false … H) …);
+ napply (or2_elim ((eq_b8 b3 b1) = false) ((eq_b8 b4 b2) = false) ? (andb_false2 … H) …);
##[ ##1: #H1; napply (decidable_w16_aux1 … (neqb8_to_neq … H1))
##| ##2: #H1; napply (decidable_w16_aux2 … (neqb8_to_neq … H1))
##]