proposition: Lemma decomp_some_head_consts s t E x y: decomp s t = Some E -> head s = const x -> head t = const y -> x = y.
proof: Proof. decomp_ind; eauto. all: 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)