- nDestructTac: Sys.break handled in two places

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

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma
index e1a64150599580ba687f254c81f3e33ce4ebe60c..5660846151ccccf34091579dec50f40f283ee317 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma
@@ -22,7 +22,7 @@ include "basic_2/computation/csn_vector.ma".
 (* Advanced properties ******************************************************)
 
 (* Basic_1: was only: sn3_appls_lref *)
-lemma csn_applv_cnf: ∀L,T. 𝐒[T] → L ⊢ 𝐍[T] → 
+lemma csn_applv_cnf: ∀L,T. 𝐒⦃T⦄ → L ⊢ 𝐍⦃T⦄ → 
                      ∀Vs. L ⊢ ⬇* Vs → L ⊢ ⬇* ⒶVs.T.
 #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(csn_cnf … H2T) ] (**) (* /2 width=1/ does not work *)
 #V #Vs #IHV #H