(* Progetto FreeScale *)
(* *)
(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Ultima modifica: 05/08/2009 *)
+(* Sviluppo: 2008-2010 *)
(* *)
(* ********************************************************************** *)
#T; #h; #t;
nnormalize;
#H;
- napply (nat_destruct_0_S ? H).
+ ndestruct (*napply (nat_destruct_0_S ? H)*).
nqed.
nlemma fold_right_list2_aux2 :
#T; #h; #t;
nnormalize;
#H;
- napply (nat_destruct_S_0 ? H).
+ ndestruct (*napply (nat_destruct_S_0 ? H)*).
nqed.
nlemma fold_right_list2_aux3 :
##[ ##1: nnormalize; #H; napply refl_eq
##| ##2: #a; #l'; #H; #H1;
nchange in H1:(%) with ((S O) = (S (S (len_list T l'))));
- nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
+ ndestruct (*nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))*)
##| ##3: #a; #l'; #H; #H1;
nchange in H1:(%) with ((S (S (len_list T l'))) = (S O));
- nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
+ ndestruct (*nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))*)
##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
nchange in H2:(%) with ((S (S (len_list T l1))) = (S (S (len_list T l))));
nchange with ((S (len_list T l1)) = (S (len_list T l)));
(* abs elem *)
ndefinition abs_list_aux1 : ∀T:Type.∀n.((len_list T []) > n) = true → False.
- #T; nnormalize; #n; #H; napply (bool_destruct … H). nqed.
+ #T; nnormalize; #n; #H; ndestruct (*napply (bool_destruct … H)*). nqed.
ndefinition abs_list_aux2 : ∀T:Type.∀h:T.∀t:list T.∀n.((len_list T (h::t)) > (S n) = true) → ((len_list T t) > n) = true.
#T; #h; #t; #n; nnormalize; #H; napply H. nqed.
nnormalize;
ncases t';
nnormalize;
- ##[ ##1: #x; #H; nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))
- ##| ##2: #x; #l; #H; nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))
+ ##[ ##1: #x; #H; ndestruct (*nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))*)
+ ##| ##2: #x; #l; #H; ndestruct (*nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))*)
##]
nqed.
nnormalize;
ncases t;
nnormalize;
- ##[ ##1: #x; #H; nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))
- ##| ##2: #x; #l; #H; nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))
+ ##[ ##1: #x; #H; ndestruct (*nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))*)
+ ##| ##2: #x; #l; #H; ndestruct (*nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))*)
##]
nqed.
(* abs elem *)
ndefinition abs_neList_aux1 : ∀T:Type.∀h:T.∀n.((len_neList T («£h»)) > (S n)) = true → False.
- #T; #h; #n; nnormalize; #H; napply (bool_destruct … H). nqed.
+ #T; #h; #n; nnormalize; #H; ndestruct (*napply (bool_destruct … H)*). nqed.
ndefinition abs_neList_aux2 : ∀T:Type.∀h:T.∀t:ne_list T.∀n.((len_neList T (h§§t)) > (S n) = true) → ((len_neList T t) > n) = true.
#T; #h; #t; #n; nnormalize; #H; napply H. nqed.