proposition: Lemma decomp_lambda_free s t E: decomp s t = Some E -> lambda_free s -> lambda_free t -> all_terms (@lambda_free X) E.
proof: Proof. decomp_ind; intros; eauto; simplify; cbn; eauto using all_terms_nil. inv H4; inv H5; intuition easy. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)