proposition: Lemma equi_unifiable_decompose_app s1 s2 t1 t2: [(s1 s2, t1 t2)] ≈ [(s1, t1); (s2, t2)].
proof: Proof. intros ?;simplify; cbn; intuition (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)