From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 22 Jul 2009 11:16:21 +0000 (+0000)
Subject: nelim fixed
X-Git-Tag: make_still_working~3636
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=633b66b935bbc2c38a5abc2be958359335123258;p=helm.git

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 5a7f658ec..81422d204 100644
--- 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