proposition: Lemma linearize_vars S: vars (linearize_terms S) === Vars S.
proof: Proof. split. - intros ? H % vars_varof. inv H. eapply varof_vars in H1. rewrite AppR_vars in H1. simplify in H1. cbn in H1; intuition idtac. discriminate. eapply in_flat_map in H as [? []]. mapinj. eapply vars_ren in H0 as []. intuition idtac. injection H1 as ->. eapply in_flat_map. eexists; eauto. - intros x H. eapply varof_vars; econstructor; eapply vars_varof. rewrite AppR_vars; simplify; right. eapply in_flat_map in H as [y]; eapply in_flat_map; exists (ren shift y). intuition (auto with listdb). now eapply ren_vars. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification)