proposition: Lemma eclosed_closed t : (forall sigma, subst sigma t = t) -> eclosed (closure [] t).
proof: Proof. move=> H. split; last done. apply /closed_dcl /closed_I. move=> ?. by rewrite L_subst_Lambda_subst. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.term_facts) Undecidability.L.Util.L_facts List Lia Relations ssreflect