From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 18 May 2008 18:22:24 +0000 (+0000)
Subject: Dummy dependent types are no longer cleaned in inductive type arities.
X-Git-Tag: make_still_working~5164
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f48faa46342b557486e06c17fd574d1eeb386239;p=helm.git

Dummy dependent types are no longer cleaned in inductive type arities.
---

diff --git a/helm/software/matita/library/list/in.ma b/helm/software/matita/library/list/in.ma
index 0e3be3a8f..d6c165022 100644
--- a/helm/software/matita/library/list/in.ma
+++ b/helm/software/matita/library/list/in.ma
@@ -99,7 +99,7 @@ lemma mem_true_to_in_list :
   \forall x,l.mem A equ x l = true \to in_list A x l.
 intros 5.elim l
   [simplify in H1;destruct H1
-  |simplify in H2;apply (bool_elim ? (equ x t))
+  |simplify in H2;apply (bool_elim ? (equ x a))
      [intro;rewrite > (H ? ? H3);apply in_list_head
      |intro;rewrite > H3 in H2;simplify in H2;
       apply in_list_cons;apply H1;assumption]]
@@ -113,14 +113,14 @@ intros 5.elim l
   [elim (not_in_list_nil ? ? H1)
   |elim H2
     [simplify;rewrite > H;reflexivity
-    |simplify;rewrite > H4;apply (bool_elim ? (equ a a1));intro;reflexivity]].
+    |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]].
 qed.
 
 lemma in_list_filter_to_p_true : \forall l,x,p.
 in_list nat x (filter nat l p) \to p x = true.
 intros 3;elim l
   [simplify in H;elim (not_in_list_nil ? ? H)
-  |simplify in H1;apply (bool_elim ? (p t));intro;rewrite > H2 in H1;
+  |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
    simplify in H1
      [elim (in_list_cons_case ? ? ? ? H1)
         [rewrite > H3;assumption
@@ -131,7 +131,7 @@ qed.
 lemma in_list_filter : \forall l,p,x.in_list nat x (filter nat l p) \to in_list nat x l.
 intros 3;elim l
   [simplify in H;elim (not_in_list_nil ? ? H)
-  |simplify in H1;apply (bool_elim ? (p t));intro;rewrite > H2 in H1;
+  |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
    simplify in H1
      [elim (in_list_cons_case ? ? ? ? H1)
         [rewrite > H3;apply in_list_head
@@ -145,7 +145,7 @@ intros 3;elim l
   [elim (not_in_list_nil ? ? H)
   |elim (in_list_cons_case ? ? ? ? H1)
      [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head
-     |simplify;apply (bool_elim ? (p t));intro;simplify;
+     |simplify;apply (bool_elim ? (p a));intro;simplify;
         [apply in_list_cons;apply H;assumption
         |apply H;assumption]]]
 qed.
diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma
index a180cbabc..ad44bd63a 100644
--- a/helm/software/matita/library/list/list.ma
+++ b/helm/software/matita/library/list/list.ma
@@ -186,13 +186,13 @@ qed.
 
 lemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
 intros (A B f g l Efg); elim l; simplify; [1: reflexivity ];
-rewrite > (Efg t); rewrite > H; reflexivity;  
+rewrite > (Efg a); rewrite > H; reflexivity;  
 qed.
 
 lemma le_length_filter : \forall A,l,p.length A (filter A l p) \leq length A l.
 intros;elim l
   [simplify;apply le_n
-  |simplify;apply (bool_elim ? (p t));intro
+  |simplify;apply (bool_elim ? (p a));intro
      [simplify;apply le_S_S;assumption
      |simplify;apply le_S;assumption]]
 qed.
\ No newline at end of file