-lemma frees_inv_lref_drops: â\88\80L,i,f. L â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89¡ f →
- â\88¨â\88¨ â\88\83â\88\83g. â¬\87*[â\92», ð\9d\90\94â\9d´iâ\9dµ] L â\89¡ â\8b\86 & ð\9d\90\88â¦\83gâ¦\84 & f = â\86\91*[i] ⫯g
- | â\88\83â\88\83g,I,K,V. K â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ g &
- â¬\87*[i] L â\89¡ K.â\93\91{I}V & f = â\86\91*[i] ⫯g
- | â\88\83â\88\83g,I,K. â¬\87*[i] L â\89¡ K.â\93¤{I} & ð\9d\90\88â¦\83gâ¦\84 & f = â\86\91*[i] ⫯g.
+lemma frees_inv_lref_drops: â\88\80L,i,f. L â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89\98 f →
+ â\88¨â\88¨ â\88\83â\88\83g. â¬\87*[â\92», ð\9d\90\94â\9d´iâ\9dµ] L â\89\98 â\8b\86 & ð\9d\90\88â¦\83gâ¦\84 & f = ⫯*[i] â\86\91g
+ | â\88\83â\88\83g,I,K,V. K â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 g &
+ â¬\87*[i] L â\89\98 K.â\93\91{I}V & f = ⫯*[i] â\86\91g
+ | â\88\83â\88\83g,I,K. â¬\87*[i] L â\89\98 K.â\93¤{I} & ð\9d\90\88â¦\83gâ¦\84 & f = ⫯*[i] â\86\91g.