X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Fcsup%2Fcsups_csups.etc;h=9978429d755ab84808e4edab7c889e68809ee34e;hb=b3c3ea1c87cbd7a87c8c29a276fc16f9ebbfb5bd;hp=aa54d9bef40636d4992ead28ec2232726ff4bccc;hpb=e8998d29ab83e7b6aa495a079193705b2f6743d3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups_csups.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups_csups.etc
index aa54d9bef..9978429d7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups_csups.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups_csups.etc
@@ -55,8 +55,3 @@ lemma lift_csups_trans_aux: ∀T1,U1,d,e. ⇧[d, e] T1 ≡ U1 →
 #L #L2 #U #U2 #HL1 #HL2 #IHL1 #H destruct
 
 * -T1 -U1 -d -e
-
-(* Main propertis ***********************************************************)
-
-theorem csups_trans: bi_transitive … csups.
-/2 width=4/ qed.