-lemma lsubv_cnv_trans (a) (h) (G):
- ∀L2,T. ⦃G, L2⦄ ⊢ T ![a,h] →
- ∀L1. G ⊢ L1 ⫃![a,h] L2 → ⦃G, L1⦄ ⊢ T ![a,h].
-#a #h #G #L2 #T #H elim H -G -L2 -T //
+lemma lsubv_cnv_trans (h) (a) (G):
+ ∀L2,T. ❨G,L2❩ ⊢ T ![h,a] →
+ ∀L1. G ⊢ L1 ⫃![h,a] L2 → ❨G,L1❩ ⊢ T ![h,a].
+#h #a #G #L2 #T #H elim H -G -L2 -T //