proposition: Lemma decomp'_irrefl E E': decomp' E = Some E' -> forall u v, (u,v) ∈ E' -> u <> v.
proof: Proof. decomp_ind. all: intuition idtac; simplify in *. subst; destruct H2; [|eauto]. eapply decomp_irrefl; eauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)