snapshot with more duality, almost where we left without duality

[helm.git] / helm / software / matita / dama / excess.ma

diff --git a/helm/software/matita/dama/excess.ma b/helm/software/matita/dama/excess.ma
index 959e866fd6bd66bf436b287c5fd023652da20628..826ae8c0bd721964f0520ddb854d48b3c75c9080 100644 (file)
--- a/helm/software/matita/dama/excess.ma
+++ b/helm/software/matita/dama/excess.ma
@@ -51,18 +51,18 @@ qed.
 
 record excess_ : Type ≝ {
   exc_exc:> excess_base;
-  exc_ap: apartness;
-  exc_with: ap_carr exc_ap = exc_carr exc_exc
+  exc_ap_: apartness;
+  exc_with: ap_carr exc_ap_ = exc_carr exc_exc
 }.
 
-definition apart_of_excess_: excess_ → apartness.
+definition exc_ap: excess_ → apartness.
 intro E; apply (mk_apartness E); unfold Type_OF_excess_; 
 cases (exc_with E); simplify;
-[apply (ap_apart (exc_ap E));
+[apply (ap_apart (exc_ap_ E));
 |apply ap_coreflexive;|apply ap_symmetric;|apply ap_cotransitive] 
 qed.
 
-coercion cic:/matita/excess/apart_of_excess_.con.
+coercion cic:/matita/excess/exc_ap.con.
 
 record excess : Type ≝ {
   excess_carr:> excess_;
@@ -245,7 +245,7 @@ intro E; apply mk_excess;
       [ apply (λx,y:E.y≰x);|apply exc_coreflexive;
       | unfold cotransitive; simplify; intros (x y z H);
         cases (exc_cotransitive E ??z H);[right|left]assumption]
-  |2: apply (exc_ap E);
+  |2: apply (exc_ap_ E);
   |3: apply (exc_with E);]
 |2: simplify; intros (y x H); fold simplify (y#x) in H;
     apply ap2exc; apply ap_symmetric; apply H;