fact: Definition eclosed_future v := match v with | (true, x) => eclosed x | (false, closure xs s) => eclosed (closure xs (lam s)) end.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun