-lemma frees_inv_bind_void: â\88\80f,p,I,L,V,T. L â\8a¢ ð\9d\90\85*â¦\83â\93\91{p,I}V.Tâ¦\84 â\89¡ f →
- â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f1 & L.â\93§ â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f2 & f1 â\8b\93 ⫱f2 â\89¡ f.
+lemma frees_inv_bind_void: â\88\80f,p,I,L,V,T. L â\8a¢ ð\9d\90\85*â¦\83â\93\91{p,I}V.Tâ¦\84 â\89\98 f →
+ â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 f1 & L.â\93§ â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f2 & f1 â\8b\93 ⫱f2 â\89\98 f.