(* 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