- nDestructTac: Sys.break handled in two places

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / computation / lsubc.ma

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 31ac81bf5442c529a86e94ceae91ee19222b87a5..bcf6c771431c79b07e956c8316ee8d0512b32723 100644 (file)
--- 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
+*)