(* Progetto FreeScale *)
(* *)
(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Ultima modifica: 05/08/2009 *)
+(* Sviluppo: 2008-2010 *)
(* *)
(* ********************************************************************** *)
(* ESADECIMALI *)
(* *********** *)
+(*
ndefinition exadecim_destruct_aux ≝
Πe1,e2.ΠP:Prop.ΠH:e1 = e2.
match eq_ex e1 e2 with [ true ⇒ P → P | false ⇒ P ].
nnormalize;
napply (λx.x).
nqed.
+*)
nlemma symmetric_andex : symmetricT exadecim exadecim and_ex.
#e1; #e2;
ncases n2;
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)
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
##]
nqed.