nelim fixed

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
index 5a7f658ec5cf1e5eb0b6547db5b730264b7b6d53..81422d2041dd0e9ba3184f4cc495cebf69aad800 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
@@ -208,9 +208,7 @@ nlemma list_destruct_nil_cons : ∀T.∀x:T.∀y:list T.nil T = cons T x y → F
 nqed.
 
 nlemma append_nil : ∀T:Type.∀l:list T.(l@[]) = l.
- #T; #l;
- (* perche' non nelim l; !!! *)
- napply (list_ind T ??? l);
+ #T; #l; nelim l;
  nnormalize;
  ##[ ##1: napply (refl_eq ??)
  ##| ##2: #x; #y; #H;
@@ -221,8 +219,7 @@ nqed.
 
 nlemma associative_list : ∀T.associative (list T) (append T).
  #T; #x; #y; #z;
- (* perche' non nelim x; !!! *)
- napply (list_ind T ??? x);
+ nelim x;
  nnormalize;
  ##[ ##1: napply (refl_eq ??)
  ##| ##2: #a; #b; #H;
@@ -242,4 +239,4 @@ nlemma append_cons_commute : ∀T:Type.∀a:T.∀l,l1:list T.l @ (a::l1) = (l@[a
  nrewrite > (associative_list T l [a] l1);
  nnormalize;
  napply (refl_eq ??).
-nqed.
+nqed.
\ No newline at end of file