proposition: Lemma decomp_none_not_unifiable sigma s t: decomp s t = None -> lambda_free s -> lambda_free t -> ~ unifies sigma s t.
proof: Proof. decomp_ind. 1 - 2: intros; destruct t; unfold unifies; cbn; solve [congruence | eauto]. 1 - 2: intros ?? _ H1 H2; inv H1; inv H2. 1 - 2: intros ???? _ H H1 H2 U; inv H1; inv H2; eapply H; eauto; unfold unifies in *; cbn in *; congruence. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)