proposition: Lemma update_irrelevant x s t sigma: ~ x ∈ vars t -> update x s sigma • t = sigma • t.
proof: Proof. intros H; eapply subst_extensional; intros y. unfold update; destruct eq_dec; now subst. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)