proposition: Lemma linearize_terms_equiv S T: linearize_terms S ≡ linearize_terms T <-> S ≡₊ T.
proof: Proof. split. - intros [? % list_equiv_anti_ren _] % equiv_lam_elim % equiv_AppR_elim; eauto. unfold shift; intros ??; congruence. - unfold linearize_terms. now intros ->. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification)