#x; nelim x; #e1; #e2;
#y; nelim y; #e3; #e4;
nnormalize;
- napply (or_elim (e1 = e3) (e1 ≠ e3) ? (decidable_ex e1 e3) …);
- ##[ ##2: #H; napply (or_intror … (decidable_b8_aux1 e1 e2 e3 e4 H))
- ##| ##1: #H; napply (or_elim (e2 = e4) (e2 ≠ e4) ? (decidable_ex e2 e4) …);
- ##[ ##2: #H1; napply (or_intror … (decidable_b8_aux2 e1 e2 e3 e4 H1))
+ napply (or2_elim (e1 = e3) (e1 ≠ e3) ? (decidable_ex e1 e3) …);
+ ##[ ##2: #H; napply (or2_intro2 … (decidable_b8_aux1 e1 e2 e3 e4 H))
+ ##| ##1: #H; napply (or2_elim (e2 = e4) (e2 ≠ e4) ? (decidable_ex e2 e4) …);
+ ##[ ##2: #H1; napply (or2_intro2 … (decidable_b8_aux2 e1 e2 e3 e4 H1))
##| ##1: #H1; nrewrite > H; nrewrite > H1;
- napply (or_introl … (refl_eq ? 〈e3,e4〉))
+ napply (or2_intro1 … (refl_eq ? 〈e3,e4〉))
##]
##]
nqed.
#e1; #e2; #e3; #e4;
nchange with ((((eq_ex e3 e1) ⊗ (eq_ex e4 e2)) = false) → ?);
#H;
- napply (or_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_false … H) …);
##[ ##1: #H1; napply (decidable_b8_aux1 … (neqex_to_neq … H1))
##| ##2: #H1; napply (decidable_b8_aux2 … (neqex_to_neq … H1))
##]
nlemma byte8_destruct : ∀e1,e2,e3,e4.〈e1,e2〉 ≠ 〈e3,e4〉 → e1 ≠ e3 ∨ e2 ≠ e4.
#e1; #e2; #e3; #e4;
nnormalize; #H;
- napply (or_elim (e1 = e3) (e1 ≠ e3) ? (decidable_ex e1 e3) …);
- ##[ ##2: #H1; napply (or_introl … H1)
- ##| ##1: #H1; napply (or_elim (e2 = e4) (e2 ≠ e4) ? (decidable_ex e2 e4) …);
- ##[ ##2: #H2; napply (or_intror … H2)
+ napply (or2_elim (e1 = e3) (e1 ≠ e3) ? (decidable_ex e1 e3) …);
+ ##[ ##2: #H1; napply (or2_intro1 … H1)
+ ##| ##1: #H1; napply (or2_elim (e2 = e4) (e2 ≠ e4) ? (decidable_ex e2 e4) …);
+ ##[ ##2: #H2; napply (or2_intro2 … H2)
##| ##1: #H2; nrewrite > H1 in H:(%);
nrewrite > H2;
#H; nelim (H (refl_eq …))
nelim b1; #e1; #e2;
nelim b2; #e3; #e4;
#H; nchange with (((eq_ex e1 e3) ⊗ (eq_ex e2 e4)) = false);
- napply (or_elim (e1 ≠ e3) (e2 ≠ e4) ? (byte8_destruct … H) …);
+ napply (or2_elim (e1 ≠ e3) (e2 ≠ e4) ? (byte8_destruct … H) …);
##[ ##1: #H1; nrewrite > (neq_to_neqex … H1); nnormalize; napply refl_eq
##| ##2: #H1; nrewrite > (neq_to_neqex … H1);
nrewrite > (symmetric_andbool (eq_ex e1 e3) false);