proposition: Lemma linearize_terms_subst sigma S: sigma • linearize_terms S = linearize_terms (sigma •₊ S).
proof: Proof. unfold linearize_terms; asimpl. rewrite !map_map; asimpl. f_equal. f_equal. eapply map_ext. intros ?; now asimpl. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification)