X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fcomputation%2Flsubc.ma;h=bcf6c771431c79b07e956c8316ee8d0512b32723;hb=5ac2dc4e01aca542ddd13c02b304c646d8df9799;hp=31ac81bf5442c529a86e94ceae91ee19222b87a5;hpb=a386e0eb6b20909ae78c825203d77647b8fde30c;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma
index 31ac81bf5..bcf6c7714 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma
@@ -101,4 +101,6 @@ lemma lsubc_refl: ∀RP,L. L ⊑[RP] L.
 #RP #L elim L -L // /2 width=1/
 qed.
 
-(* Basic_1: removed theorems 2: csubc_clear_conf csubc_getl_conf *)
+(* Basic_1: removed theorems 3:
+            csubc_clear_conf csubc_getl_conf csubc_csuba
+*)