...

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
index 228692451a5d3637bd8a1a95d17edc3c7bfd3849..3e108e7bebb4620ae15957f7cd2979aabf134516 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
@@ -66,8 +66,7 @@ nlemma absurd : ∀A,C:Prop.A → ¬A → C.
  #A; #C; #H;
  nnormalize;
  #H1;
- (* perche' non fa nelim (H1 H). ??? *)
- napply (False_ind ? (H1 H)).
+ nelim (H1 H);
 nqed.
 
 nlemma not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
@@ -190,18 +189,15 @@ nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
  #A;
  nnormalize;
  #x; #y; #H;
- (* rifiuta nrewrite >, nrewrite <
-    e la prima volta mi ha risposto con assert false,
-    poi con errori di tipo ??? *) 
  nrewrite < H;
  napply (refl_eq ??).
 nqed.
 
 nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
  #A; #x; #P; #H; #y; #H1;
- napply (eq_ind ? x ? H y ?);
- nrewrite < H1;
- napply (refl_eq ??).
+ nletin H2 ≝ (symmetric_eq ??? H1);
+ nrewrite < H2;
+ nassumption.
 nqed.
 
 ndefinition relationT : Type → Type → Type ≝
@@ -219,15 +215,6 @@ ninductive list (A:Type) : Type ≝
   nil: list A
 | cons: A -> list A -> list A.
 
-nlet rec list_ind (A:Type) (P:list A → Prop) (p:P (nil A)) (f:(Πa:A.Πl':list A.P l' → P (cons A a l'))) (l:list A) on l ≝
- match l with [ nil ⇒ p | cons h t ⇒ f h t (list_ind A P p f t) ].
-
-nlet rec list_rec (A:Type) (P:list A → Set) (p:P (nil A)) (f:Πa:A.Πl':list A.P l' → P (cons A a l')) (l:list A) on l ≝
- match l with [ nil ⇒ p | cons h t ⇒ f h t (list_rec A P p f t) ].
-
-nlet rec list_rect (A:Type) (P:list A → Type) (p:P (nil A)) (f:Πa:A.Πl':list A.P l' → P (cons A a l')) (l:list A) on l ≝
- match l with [ nil ⇒ p | cons h t ⇒ f h t (list_rect A P p f t) ].
-
 nlet rec append A (l1: list A) l2 on l1 ≝
  match l1 with
   [ nil => l2