frst step to move away the CoRN stuff

[helm.git] / helm / software / matita / library / algebra / CoRN / SetoidFun.ma

diff --git a/helm/software/matita/library/algebra/CoRN/SetoidFun.ma b/helm/software/matita/library/algebra/CoRN/SetoidFun.ma
index 67f8ac1d6a5763dfab65e15b17128ed1d3f66b85..ad16edf7bf6c5f6fc6611e184ac6ab1814e30b32 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.
@@ -473,7 +473,7 @@ simplify.
 right. apply I|intros (a at).simplify. left. apply I]]
 simplify.
 left.
-autobatch new|intros 2 (c l).
+autobatch |intros 2 (c l).
 intros 2 (Hy).
 elim y 0[
 intros 2 (H z).
@@ -509,15 +509,15 @@ unfold Not.
 elim x 0[
   intro y.
   elim y 0[
-    split[simplify.intro.autobatch new|simplify.intros.exact H1]|
+    split[simplify.intro.autobatch|simplify.intros.exact H1]|
 intros (a at).
 simplify.
-split[intro.autobatch new|intros. exact H1]
+split[intro.autobatch|intros. exact H1]
 ]
 |
 intros (a at IHx).
 elim y 0[simplify.
-  split[intro.autobatch new|intros.exact H]
+  split[intro.autobatch|intros.exact H]
   |
 intros 2 (c l).
 generalize in match (IHx l).
@@ -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;