(* ********************************************************************** *)
(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
(* *)
(* ********************************************************************** *)
(* ESADECIMALI *)
(* *********** *)
-ndefinition exadecim_destruct1 : Πe2.ΠP:Prop.ΠH:x0 = e2.match e2 with [ x0 ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##1: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match x0 with [ x0 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct2 : Πe2.ΠP:Prop.ΠH:x1 = e2.match e2 with [ x1 ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##2: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match x1 with [ x1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct3 : Πe2.ΠP:Prop.ΠH:x2 = e2.match e2 with [ x2 ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##3: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match x2 with [ x2 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct4 : Πe2.ΠP:Prop.ΠH:x3 = e2.match e2 with [ x3 ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##4: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match x3 with [ x3 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct5 : Πe2.ΠP:Prop.ΠH:x4 = e2.match e2 with [ x4 ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##5: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match x4 with [ x4 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct6 : Πe2.ΠP:Prop.ΠH:x5 = e2.match e2 with [ x5 ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##6: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match x5 with [ x5 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct7 : Πe2.ΠP:Prop.ΠH:x6 = e2.match e2 with [ x6 ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##7: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match x6 with [ x6 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct8 : Πe2.ΠP:Prop.ΠH:x7 = e2.match e2 with [ x7 ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##8: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match x7 with [ x7 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct9 : Πe2.ΠP:Prop.ΠH:x8 = e2.match e2 with [ x8 ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##9: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match x8 with [ x8 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct10 : Πe2.ΠP:Prop.ΠH:x9 = e2.match e2 with [ x9 ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##10: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match x9 with [ x9 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct11 : Πe2.ΠP:Prop.ΠH:xA = e2.match e2 with [ xA ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##11: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match xA with [ xA ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct12 : Πe2.ΠP:Prop.ΠH:xB = e2.match e2 with [ xB ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##12: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match xB with [ xB ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct13 : Πe2.ΠP:Prop.ΠH:xC = e2.match e2 with [ xC ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##13: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match xC with [ xC ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct14 : Πe2.ΠP:Prop.ΠH:xD = e2.match e2 with [ xD ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##14: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match xD with [ xD ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct15 : Πe2.ΠP:Prop.ΠH:xE = e2.match e2 with [ xE ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##15: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match xE with [ xE ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct16 : Πe2.ΠP:Prop.ΠH:xF = e2.match e2 with [ xF ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##16: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match xF with [ xF ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
+(*
ndefinition exadecim_destruct_aux ≝
Πe1,e2.ΠP:Prop.ΠH:e1 = e2.
- match e1 with
- [ x0 ⇒ match e2 with [ x0 ⇒ P → P | _ ⇒ P ]
- | x1 ⇒ match e2 with [ x1 ⇒ P → P | _ ⇒ P ]
- | x2 ⇒ match e2 with [ x2 ⇒ P → P | _ ⇒ P ]
- | x3 ⇒ match e2 with [ x3 ⇒ P → P | _ ⇒ P ]
- | x4 ⇒ match e2 with [ x4 ⇒ P → P | _ ⇒ P ]
- | x5 ⇒ match e2 with [ x5 ⇒ P → P | _ ⇒ P ]
- | x6 ⇒ match e2 with [ x6 ⇒ P → P | _ ⇒ P ]
- | x7 ⇒ match e2 with [ x7 ⇒ P → P | _ ⇒ P ]
- | x8 ⇒ match e2 with [ x8 ⇒ P → P | _ ⇒ P ]
- | x9 ⇒ match e2 with [ x9 ⇒ P → P | _ ⇒ P ]
- | xA ⇒ match e2 with [ xA ⇒ P → P | _ ⇒ P ]
- | xB ⇒ match e2 with [ xB ⇒ P → P | _ ⇒ P ]
- | xC ⇒ match e2 with [ xC ⇒ P → P | _ ⇒ P ]
- | xD ⇒ match e2 with [ xD ⇒ P → P | _ ⇒ P ]
- | xE ⇒ match e2 with [ xE ⇒ P → P | _ ⇒ P ]
- | xF ⇒ match e2 with [ xF ⇒ P → P | _ ⇒ P ]
- ].
+ match eq_ex e1 e2 with [ true ⇒ P → P | false ⇒ P ].
ndefinition exadecim_destruct : exadecim_destruct_aux.
- #e1; ncases e1;
- ##[ ##1: napply exadecim_destruct1
- ##| ##2: napply exadecim_destruct2
- ##| ##3: napply exadecim_destruct3
- ##| ##4: napply exadecim_destruct4
- ##| ##5: napply exadecim_destruct5
- ##| ##6: napply exadecim_destruct6
- ##| ##7: napply exadecim_destruct7
- ##| ##8: napply exadecim_destruct8
- ##| ##9: napply exadecim_destruct9
- ##| ##10: napply exadecim_destruct10
- ##| ##11: napply exadecim_destruct11
- ##| ##12: napply exadecim_destruct12
- ##| ##13: napply exadecim_destruct13
- ##| ##14: napply exadecim_destruct14
- ##| ##15: napply exadecim_destruct15
- ##| ##16: napply exadecim_destruct16
- ##]
-nqed.
-
-nlemma symmetric_eqex : symmetricT exadecim bool eq_ex.
- #e1; #e2;
+ #e1; #e2; #P; #H;
+ nrewrite < H;
nelim e1;
- nelim e2;
nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma symmetric_andex : symmetricT exadecim exadecim and_ex.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma associative_andex : ∀e1,e2,e3.(and_ex (and_ex e1 e2) e3) = (and_ex e1 (and_ex e2 e3)).
- #e1; #e2; #e3;
- nelim e1;
- ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##]
-nqed.
-
-nlemma symmetric_orex : symmetricT exadecim exadecim or_ex.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma associative_orex : ∀e1,e2,e3.(or_ex (or_ex e1 e2) e3) = (or_ex e1 (or_ex e2 e3)).
- #e1; #e2; #e3;
- nelim e1;
- ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##]
+ napply (λx.x).
nqed.
+*)
-nlemma symmetric_xorex : symmetricT exadecim exadecim xor_ex.
- #e1; #e2;
- nelim e1;
- nelim e2;
+nlemma eq_to_eqex : ∀n1,n2.n1 = n2 → eq_ex n1 n2 = true.
+ #n1; #n2; #H;
+ nrewrite > H;
+ nelim n2;
nnormalize;
napply refl_eq.
nqed.
-nlemma associative_xorex : ∀e1,e2,e3.(xor_ex (xor_ex e1 e2) e3) = (xor_ex e1 (xor_ex e2 e3)).
- #e1; #e2; #e3;
- nelim e1;
- ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
+nlemma neqex_to_neq : ∀n1,n2.eq_ex n1 n2 = false → n1 ≠ n2.
+ #n1; #n2; #H;
+ napply (not_to_not (n1 = n2) (eq_ex n1 n2 = true) …);
+ ##[ ##1: napply (eq_to_eqex n1 n2)
+ ##| ##2: napply (eqfalse_to_neqtrue … H)
##]
nqed.
-nlemma symmetric_plusex_dc_dc : ∀e1,e2,c.plus_ex_dc_dc e1 e2 c = plus_ex_dc_dc e2 e1 c.
- #e1; #e2; #c;
- nelim e1;
- nelim e2;
- nelim c;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma plusex_dc_dc_to_dc_d : ∀e1,e2,c.fst … (plus_ex_dc_dc e1 e2 c) = plus_ex_dc_d e1 e2 c.
- #e1; #e2; #c;
- nelim e1;
- nelim e2;
- nelim c;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma plusex_dc_dc_to_dc_c : ∀e1,e2,c.snd … (plus_ex_dc_dc e1 e2 c) = plus_ex_dc_c e1 e2 c.
- #e1; #e2; #c;
- nelim e1;
- nelim e2;
- nelim c;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma plusex_dc_dc_to_d_dc : ∀e1,e2.plus_ex_dc_dc e1 e2 false = plus_ex_d_dc e1 e2.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma plusex_dc_dc_to_d_d : ∀e1,e2.fst … (plus_ex_dc_dc e1 e2 false) = plus_ex_d_d e1 e2.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma plusex_dc_dc_to_d_c : ∀e1,e2.snd … (plus_ex_dc_dc e1 e2 false) = plus_ex_d_c e1 e2.
- #e1; #e2;
- nelim e1;
- nelim e2;
+nlemma eqex_to_eq : ∀n1,n2.eq_ex n1 n2 = true → n1 = n2.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma symmetric_plusex_dc_d : ∀e1,e2,c.plus_ex_dc_d e1 e2 c = plus_ex_dc_d e2 e1 c.
- #e1; #e2; #c;
- nelim e1;
- nelim e2;
- nelim c;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma symmetric_plusex_dc_c : ∀e1,e2,c.plus_ex_dc_c e1 e2 c = plus_ex_dc_c e2 e1 c.
- #e1; #e2; #c;
- nelim e1;
- nelim e2;
- nelim c;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma symmetric_plusex_d_dc : ∀e1,e2.plus_ex_d_dc e1 e2 = plus_ex_d_dc e2 e1.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma plusex_d_dc_to_d_d : ∀e1,e2.fst … (plus_ex_d_dc e1 e2) = plus_ex_d_d e1 e2.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma plusex_d_dc_to_d_c : ∀e1,e2.snd … (plus_ex_d_dc e1 e2) = plus_ex_d_c e1 e2.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma symmetric_plusex_d_d : ∀e1,e2.plus_ex_d_d e1 e2 = plus_ex_d_d e2 e1.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma associative_plusex_d_d : ∀e1,e2,e3.(plus_ex_d_d (plus_ex_d_d e1 e2) e3) = (plus_ex_d_d e1 (plus_ex_d_d e2 e3)).
- #e1; #e2; #e3;
- nelim e1;
- ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
##]
nqed.
-nlemma symmetric_plusex_d_c : ∀e1,e2.plus_ex_d_c e1 e2 = plus_ex_d_c e2 e1.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
+nlemma neq_to_neqex : ∀n1,n2.n1 ≠ n2 → eq_ex n1 n2 = false.
+ #n1; #n2; #H;
+ napply (neqtrue_to_eqfalse (eq_ex n1 n2));
+ napply (not_to_not (eq_ex n1 n2 = true) (n1 = n2) ? H);
+ napply (eqex_to_eq n1 n2).
nqed.
-nlemma eqex_to_eq : ∀e1,e2:exadecim.(eq_ex e1 e2 = true) → (e1 = e2).
- #e1; #e2;
- ncases e1;
- ncases e2;
- nnormalize;
- ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+nlemma decidable_ex : ∀x,y:exadecim.decidable (x = y).
+ #x; #y; nnormalize;
+ napply (or2_elim (eq_ex x y = true) (eq_ex x y = false) ? (decidable_bexpr ?));
+ ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqex_to_eq … H))
+ ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqex_to_neq … H))
##]
nqed.
-nlemma eq_to_eqex : ∀e1,e2.e1 = e2 → eq_ex e1 e2 = true.
- #m1; #m2;
- ncases m1;
- ncases m2;
- nnormalize;
- ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
- ##| ##*: #H; napply (exadecim_destruct … H)
+nlemma symmetric_eqex : symmetricT exadecim bool eq_ex.
+ #n1; #n2;
+ napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_ex n1 n2));
+ ##[ ##1: #H; nrewrite > H; napply refl_eq
+ ##| ##2: #H; nrewrite > (neq_to_neqex n1 n2 H);
+ napply (symmetric_eq ? (eq_ex n2 n1) false);
+ napply (neq_to_neqex n2 n1 (symmetric_neq ? n1 n2 H))
##]
nqed.
projects / helm.git / blobdiff