- the relation for pointwise extensions now takes a binder as argument

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / lsubsv_snv.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma
index dcf7b73478858d26ccc6f070ccde0e283a67de89..e4596e7d4fb57e7becab9f5ac4c8a5c53845a079 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma
@@ -22,7 +22,7 @@ include "basic_2/dynamic/lsubsv_cpcs.ma".
 (* Properties concerning stratified native validity *************************)
 
 lemma lsubsv_snv_trans: ∀h,g,G,L2,T. ⦃G, L2⦄ ⊢ T ¡[h, g] →
-                        â\88\80L1. G â\8a¢ L1 ¡â\8a\91[h, g] L2 → ⦃G, L1⦄ ⊢ T ¡[h, g].
+                        â\88\80L1. G â\8a¢ L1 ¡â«\83[h, g] L2 → ⦃G, L1⦄ ⊢ T ¡[h, g].
 #h #g #G #L2 #T #H elim H -G -L2 -T //
 [ #I #G #L2 #K2 #V #i #HLK2 #_ #IHV #L1 #HL12
   elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1