(* ********************************************************************** *)
(* 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 *)
(* *)
(* ********************************************************************** *)
napply refl_eq.
nqed.
+(* !!! da togliere *)
nlemma list_destruct_cons_nil : ∀T.∀x:T.∀y:list T.cons T x y = nil T → False.
#T; #x; #y; #H;
nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
napply I.
nqed.
+(* !!! da togliere *)
nlemma list_destruct_nil_cons : ∀T.∀x:T.∀y:list T.nil T = cons T x y → False.
#T; #x; #y; #H;
nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
napply refl_eq.
nqed.
+(* !!! da togliere *)
nlemma nelist_destruct_cons_nil : ∀T.∀x1,x2:T.∀y1:ne_list T.ne_cons T x1 y1 = ne_nil T x2 → False.
#T; #x1; #x2; #y1; #H;
nchange with (match ne_cons T x1 y1 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]);
napply I.
nqed.
+(* !!! da togliere *)
nlemma nelist_destruct_nil_cons : ∀T.∀x1,x2:T.∀y2:ne_list T.ne_nil T x1 = ne_cons T x2 y2 → False.
#T; #x1; #x2; #y2; #H;
nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]);