proposition: Lemma it_up_free' k (sigma: fin -> exp X): free' (free k) (it k up sigma).
proof: Proof. unfold free; split; intros x; unfold bound. - intros ?; rewrite it_up_lt; intuition idtac. lia. - intros ? y. rewrite it_up_ge; eauto. intros [z [->]] % vars_varof % varof_ren; eauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)