update in basic_2 ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / csup / csups_csups.etc

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 aa54d9bef40636d4992ead28ec2232726ff4bccc..9978429d755ab84808e4edab7c889e68809ee34e 100644 (file)
--- 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.