-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