-lemma cnv_lref_drops (a) (h) (G):
- â\88\80I,K,V,i,L. â¦\83G,Kâ¦\84 â\8a¢ V ![a,h] →
- â¬\87*[i] L â\89\98 K.â\93\91{I}V â\86\92 â¦\83G,Lâ¦\84 â\8a¢ #i ![a,h].
-#a #h #G #I #K #V #i elim i -i
+lemma cnv_lref_drops (h) (a) (G):
+ â\88\80I,K,V,i,L. â\9d¨G,Kâ\9d© â\8a¢ V ![h,a] →
+ â\87©[i] L â\89\98 K.â\93\91[I]V â\86\92 â\9d¨G,Lâ\9d© â\8a¢ #i ![h,a].
+#h #a #G #I #K #V #i elim i -i