proposition: Lemma decomp'_lambda_free E E': decomp' E = Some E' -> all_terms (@lambda_free X) E -> all_terms (@lambda_free X) E'.
proof: Proof. decomp_ind; intros; eauto; simplify in *; intuition idtac. eapply decomp_lambda_free in H; firstorder. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)