-fact frees_inv_bind_aux: โf,L,X. L โข ๐
*โฆXโฆ โ f โ โp,I,V,T. X = โ{p,I}V.T โ
- โโf1,f2. L โข ๐
*โฆVโฆ โ f1 & L.โ{I}V โข ๐
*โฆTโฆ โ f2 & f1 โ โซฑf2 โ f.
+fact frees_inv_bind_aux:
+ โf,L,X. L โข ๐
+โฆXโฆ โ f โ โp,I,V,T. X = โ{p,I}V.T โ
+ โโf1,f2. L โข ๐
+โฆVโฆ โ f1 & L.โ{I}V โข ๐
+โฆTโฆ โ f2 & f1 โ โซฑf2 โ f.