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