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

diff --git a/helm/software/matita/library/algebra/CoRN/SemiGroups.ma b/helm/software/matita/library/algebra/CoRN/SemiGroups.ma
index b57d3b2fde5f22d2a735e277df8be2f35090d085..8613d83e2ba486c110c817fed6107ef41c33179b 100644 (file)
--- a/helm/software/matita/library/algebra/CoRN/SemiGroups.ma
+++ b/helm/software/matita/library/algebra/CoRN/SemiGroups.ma
@@ -187,8 +187,8 @@ lemma part_function_plus_strext :  \forall G:CSemiGroup. \forall F,F': PartFunct
   \to x \neq y.
 intros (G F F' x y Hx Hy H).
 elim (bin_op_strext_unfolded ? ? ? ? ? ? H)[
-apply pfstrx[apply F|elim Hx.apply t|elim Hy.apply t|exact H1]|
-apply pfstrx[apply F'|elim Hx.apply t1|elim Hy.apply t1|exact H1]]
+apply pfstrx[apply F|elim Hx.apply a|elim Hy.apply a|exact H1]|
+apply pfstrx[apply F'|elim Hx.apply b|elim Hy.apply b|exact H1]]
 qed.
 
 definition Fplus : \forall G:CSemiGroup. \forall F,F': PartFunct G. ? \def 

diff --git a/helm/software/matita/library/algebra/CoRN/SetoidFun.ma b/helm/software/matita/library/algebra/CoRN/SetoidFun.ma
index 67f8ac1d6a5763dfab65e15b17128ed1d3f66b85..9fb4073bac8730da01aa0b78d5745f590ade3e38 100644 (file)
--- a/helm/software/matita/library/algebra/CoRN/SetoidFun.ma
+++ b/helm/software/matita/library/algebra/CoRN/SetoidFun.ma
@@ -421,7 +421,7 @@ unfold Not.
 intro.
 unfold in H.
 apply False_ind.
-apply H1.apply t.
+apply H1.apply a.
 exact H2|exact H2]
 ]
 qed.
@@ -677,7 +677,7 @@ lemma conj_wd : \forall S:CSetoid. \forall P,Q : S \to Type.
   unfold pred_wd.
   unfold conjP.
   intros.elim c.
-  split [ apply (f x ? t).assumption|apply (f1 x ? t1). assumption]
+  split [ apply (f x ? a).assumption|apply (f1 x ? b). assumption]
 qed.
 
 (* End Conjunction. *)
@@ -754,7 +754,7 @@ lemma ext2_a : \forall S:CSetoid. \forall P: S \to Prop.
 intros.
 elim e.
 apply (existT).assumption.
-apply (t1 t).
+apply (b a).
 qed.
 
 (*
@@ -827,7 +827,7 @@ intros (S P R H H0).
 unfold.
 intros (x y H1 H2).
 elim H1;split[apply (H x).assumption. exact H2|
-  intro H5.apply (H0 x ? t)[apply H2|apply t1]
+  intro H5.apply (H0 x ? a)[apply H2|apply b]
   ]
 qed.
 
@@ -1272,8 +1272,8 @@ lemma Inv_bij : \forall A, B:CSetoid.
   bijective ? ?  (inverse A B f).
  intros;
  elim f 2;
- elim c2 0;
- elim c3 0;
+ elim c 0;
+ elim c1 0;
  simplify;
  intros;
  split;

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index 4c51d3a448e15a900e8b28f2118cb480139614fd..35f3b0920cba32c03d5887e149a592bda7207999 100644 (file)
--- a/helm/software/matita/library/technicalities/setoids.ma
+++ b/helm/software/matita/library/technicalities/setoids.ma
@@ -86,8 +86,8 @@ definition Arguments := nelistT Argument_Class.
 definition function_type_of_morphism_signature :
  Arguments → Relation_Class → Type.
   intros (In Out); elim In; 
-  [ exact (carrier_of_relation_class ? t → carrier_of_relation_class ? Out)
-  | exact (carrier_of_relation_class ? t → T)
+  [ exact (carrier_of_relation_class ? a → carrier_of_relation_class ? Out)
+  | exact (carrier_of_relation_class ? a → T)
   ]
 qed. 
 
@@ -99,24 +99,24 @@ definition make_compatibility_goal_aux:
  generalize in match f; clear f;
   [ elim a; simplify in f f1;
      [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
-     | cases t;
+     | cases x;
         [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
         | exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2))
         ]
      | exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
-     | cases t;
+     | cases x;
         [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
         | exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2))
         ]
      | exact (∀x. relation_of_relation_class ? Out (f x) (f1 x))
      ]
   | change with
-     ((carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) →
-      (carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) →
+     ((carrier_of_relation_class ? a → function_type_of_morphism_signature n Out) →
+      (carrier_of_relation_class ? a → function_type_of_morphism_signature n Out) →
       Prop).
-    elim t; simplify in f f1;
+    elim a; simplify in f f1;
      [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
-     |2,4: cases t1;
+     |2,4: cases x;
         [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
         |2,4: exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2))
         ]
@@ -136,8 +136,8 @@ record Morphism_Theory (In: Arguments) (Out: Relation_Class) : Type :=
 definition list_of_Leibniz_of_list_of_types: nelistT Type → Arguments.
  intro;
  elim n;
-  [ apply (singl ? (Leibniz ? t))
-  | apply (cons ? (Leibniz ? t) a)
+  [ apply (singl ? (Leibniz ? a))
+  | apply (cons ? (Leibniz ? a) a1)
   ]
 qed.
 
@@ -367,9 +367,9 @@ definition variance_of_argument_class : Argument_Class → option variance.
  intros;
  elim a;
   [ apply None
-  | apply (Some ? t)
+  | apply (Some ? x)
   | apply None
-  | apply (Some ? t)
+  | apply (Some ? x)
   | apply None
   ]
 qed.
@@ -569,8 +569,8 @@ in F0.
 definition product_of_arguments : Arguments → Type.
  intro;
  elim a;
-  [ apply (carrier_of_relation_class ? t)
-  | apply (Prod (carrier_of_relation_class ? t) T)
+  [ apply (carrier_of_relation_class ? a1)
+  | apply (Prod (carrier_of_relation_class ? a1) T)
   ]
 qed.
 
@@ -611,15 +611,15 @@ definition relation_of_product_of_arguments:
  elim In 0;
   [ simplify;
     intro;
-    exact (directed_relation_of_argument_class (get_rewrite_direction r t) t)
+    exact (directed_relation_of_argument_class (get_rewrite_direction r a) a)
   | intros;
-    change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
-    change in p1 with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
+    change in p with (Prod (carrier_of_relation_class variance a) (product_of_arguments n));
+    change in p1 with (Prod (carrier_of_relation_class variance a) (product_of_arguments n));
     cases p (c p2);
     cases p1 (c1 p3);
    apply And;
     [ exact
-      (directed_relation_of_argument_class (get_rewrite_direction r t) t c c1)
+      (directed_relation_of_argument_class (get_rewrite_direction r a) a c c1)
     | exact (R p2 p3)
     ]
   ]
@@ -631,10 +631,10 @@ definition apply_morphism:
  intro;
  elim In;
   [ exact (f p)
-  | change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
+  | change in p with (Prod (carrier_of_relation_class variance a) (product_of_arguments n));
    elim p;
-   change in f1 with (carrier_of_relation_class variance t → function_type_of_morphism_signature n Out);
-   exact (f ? (f1 t1) t2)
+   change in f1 with (carrier_of_relation_class variance a → function_type_of_morphism_signature n Out);
+   exact (f ? (f1 a1) b)
   ]
 qed.
 
@@ -651,14 +651,14 @@ theorem apply_morphism_compatibility_Right2Left:
    [ simplify in m1 m2 args1 args2 ⊢ %;
      change in H1 with
       (directed_relation_of_argument_class
-        (get_rewrite_direction Right2Left t) t args1 args2);
+        (get_rewrite_direction Right2Left a) a args1 args2);
      generalize in match H1; clear H1;
      generalize in match H; clear H;
      generalize in match args2; clear args2;
      generalize in match args1; clear args1;
      generalize in match m2; clear m2;
      generalize in match m1; clear m1;
-     elim t 0; simplify;
+     elim a 0; simplify;
       [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
         apply H;
         exact H1
@@ -682,32 +682,32 @@ theorem apply_morphism_compatibility_Right2Left:
         exact H1
       ]
    | change in m1 with
-      (carrier_of_relation_class variance t →
+      (carrier_of_relation_class variance a →
         function_type_of_morphism_signature n Out);
      change in m2 with
-      (carrier_of_relation_class variance t →
+      (carrier_of_relation_class variance a →
         function_type_of_morphism_signature n Out);
      change in args1 with
-      ((carrier_of_relation_class ? t) × (product_of_arguments n));
+      ((carrier_of_relation_class ? a) × (product_of_arguments n));
      change in args2 with
-      ((carrier_of_relation_class ? t) × (product_of_arguments n));
+      ((carrier_of_relation_class ? a) × (product_of_arguments n));
      generalize in match H2; clear H2;
      elim args2 0; clear args2;
      elim args1; clear args1;
      simplify in H2;
      change in H2:(? ? %) with 
-       (relation_of_product_of_arguments Right2Left n t2 t4);
+       (relation_of_product_of_arguments Right2Left n b b1);
      elim H2; clear H2;
      change with
-      (relation_of_relation_class unit Out (apply_morphism n Out (m1 t3) t4)
-        (apply_morphism n Out (m2 t1) t2));
+      (relation_of_relation_class unit Out (apply_morphism n Out (m1 a2) b1)
+        (apply_morphism n Out (m2 a1) b));
      generalize in match H3; clear H3;
-     generalize in match t3; clear t3;
-     generalize in match t1; clear t1;
+     generalize in match a1; clear a1;
+     generalize in match a2; clear a2;
      generalize in match H1; clear H1;
      generalize in match m2; clear m2;
      generalize in match m1; clear m1;
-     elim t 0;
+     elim a 0;
       [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
         simplify in H3;
         change in H1 with
@@ -772,14 +772,14 @@ theorem apply_morphism_compatibility_Left2Right:
   elim In 0; simplify; intros;
    [ change in H1 with
       (directed_relation_of_argument_class
-        (get_rewrite_direction Left2Right t) t args1 args2);
+        (get_rewrite_direction Left2Right a) a args1 args2);
      generalize in match H1; clear H1;
      generalize in match H; clear H;
      generalize in match args2; clear args2;
      generalize in match args1; clear args1;
      generalize in match m2; clear m2;
      generalize in match m1; clear m1;
-     elim t 0; simplify;
+     elim a 0; simplify;
       [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
         apply H;
         exact H1
@@ -805,31 +805,31 @@ theorem apply_morphism_compatibility_Left2Right:
         exact H1
       ]
    | change in m1 with
-      (carrier_of_relation_class variance t →
+      (carrier_of_relation_class variance a →
         function_type_of_morphism_signature n Out);
      change in m2 with
-      (carrier_of_relation_class variance t →
+      (carrier_of_relation_class variance a →
         function_type_of_morphism_signature n Out);
      change in args1 with
-      ((carrier_of_relation_class ? t) × (product_of_arguments n));
+      ((carrier_of_relation_class ? a) × (product_of_arguments n));
      change in args2 with
-      ((carrier_of_relation_class ? t) × (product_of_arguments n));
+      ((carrier_of_relation_class ? a) × (product_of_arguments n));
      generalize in match H2; clear H2;
      elim args2 0; clear args2;
      elim args1; clear args1;
      simplify in H2; change in H2:(? ? %) with
-       (relation_of_product_of_arguments Left2Right n t2 t4); 
+       (relation_of_product_of_arguments Left2Right n b b1); 
      elim H2; clear H2;
      change with
-      (relation_of_relation_class unit Out (apply_morphism n Out (m1 t1) t2)
-        (apply_morphism n Out (m2 t3) t4));
+      (relation_of_relation_class unit Out (apply_morphism n Out (m1 a1) b)
+        (apply_morphism n Out (m2 a2) b1));
      generalize in match H3; clear H3;
-     generalize in match t3; clear t3;
-     generalize in match t1; clear t1;
+     generalize in match a2; clear a2;
+     generalize in match a1; clear a1;
      generalize in match H1; clear H1;
      generalize in match m2; clear m2;
      generalize in match m1; clear m1;
-     elim t 0;
+     elim a 0;
       [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
         change in H1 with
          (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));