-/3 width=3 by lsubsv_fwd_lsubss, lsubss_xprs_trans/ qed-.
-*)
-axiom lsubsv_snv_trans: ∀h,g,L2,T. ⦃h, L2⦄ ⊩ T :[g] →
- ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → ⦃h, L1⦄ ⊩ T :[g].
-(*
-#h #g #L2 #T #H elim H -L2 -T //
-[ #I2 #L2 #K2 #V2 #i #HLK2 #_ #IHV2 #L1 #HL12
- elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
- elim (lsubsv_inv_pair2 … H) -H * #K1 [ | -IHV2 ]
- [ #HK12 #H destruct /3 width=5/
- | #V1 #l #HV1 #_ #_ #_ #H destruct /2 width=5/
+fact snv_lsubsv_aux: ∀h,g,L0,T0.
+ (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
+ (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
+ (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
+ (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) →
+ ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_lsubsv h g L1 T1.
+#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L2 * * [||||*] //
+[ #i #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2
+ elim (snv_inv_lref … H) -H #I2 #K2 #W2 #HLK2 #HW2
+ elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -HL12 #X #H #HLK1
+ lapply (ldrop_pair2_fwd_fw … HLK2 (#i)) -HLK2 #HLK2
+ elim (lsubsv_inv_pair2 … H) -H * #K1
+ [ #HK12 #H destruct /4 width=8 by snv_lref, fw_ygt/ (**) (* auto too slow without trace *)
+ | #W1 #V1 #V2 #l #HV1 #_ #_ #_ #_ #_ #H #_ destruct /2 width=5/