-lemma cnv_lref_drops (a) (h) (G): ∀I,K,V,i,L. ⦃G,K⦄ ⊢ V ![a,h] →
- ⬇*[i] L ≘ K.ⓑ{I}V → ⦃G,L⦄ ⊢ #i ![a,h].
-#a #h #G #I #K #V #i elim i -i
+lemma cnv_lref_drops (h) (a) (G):
+ ∀I,K,V,i,L. ❪G,K❫ ⊢ V ![h,a] →
+ ⇩[i] L ≘ K.ⓑ[I]V → ❪G,L❫ ⊢ #i ![h,a].
+#h #a #G #I #K #V #i elim i -i