X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fdama%2Fexcedence.ma;fp=matita%2Fdama%2Fexcedence.ma;h=6d1fc4dd7cf1c292541e963c1b15c051ef564060;hb=2030804124914a9b2155c911d4b835fd67c26d4e;hp=d91c61170f10862ec14abf62f38ccb26f51e54b4;hpb=47173a864325b6bcaf2d3cb70afcd14be97764ae;p=helm.git

diff --git a/matita/dama/excedence.ma b/matita/dama/excedence.ma
index d91c61170..6d1fc4dd7 100644
--- a/matita/dama/excedence.ma
+++ b/matita/dama/excedence.ma
@@ -104,8 +104,7 @@ lemma lt_coreflexive: ∀E.coreflexive ? (lt E).
 intros 2 (E x); intro H; cases H (_ ABS); 
 apply (ap_coreflexive ? x ABS);
 qed.
-
-(* 
+ 
 lemma lt_transitive: ∀E.transitive ? (lt E).
 intros (E); unfold; intros (x y z H1 H2); cases H1 (Lxy Axy); cases H2 (Lyz Ayz); 
 split; [apply (le_transitive ???? Lxy Lyz)] clear H1 H2;
@@ -120,5 +119,3 @@ theorem lt_to_excede: ∀E:excedence.∀a,b:E. (a < b) → (b ≰ a).
 intros (E a b Lab); cases Lab (LEab Aab);
 cases Aab (H H); [cases (LEab H)] fold normalize (b ≰ a); assumption; (* BUG *)  
 qed.
-
-*)
\ No newline at end of file