-lemma liftsv_applv: â\88\80V1s,V2s,des. â\87\91[des] V1s ≡ V2s →
- â\88\80T1,T2. â\87\91[des] T1 ≡ T2 →
- â\87\91[des] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2.
+lemma liftsv_applv: â\88\80V1s,V2s,des. â\87§*[des] V1s ≡ V2s →
+ â\88\80T1,T2. â\87§*[des] T1 ≡ T2 →
+ â\87§*[des] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2.