proposition: Lemma size_subst tau s: size (tau • s) = size s + Sum (map (tau >> size) (vars s)).
proof: Proof. induction s in tau |-*; cbn; simplify; trivial. - rewrite IHs. f_equal. f_equal. clear IHs. generalize (vars s) as A. induction A as [|[] ?]; cbn; eauto. + destruct eq_dec; rewrite IHA; easy. + destruct eq_dec; rewrite IHA. lia. cbn. unfold funcomp at 1; now rewrite size_ren. - rewrite IHs1, IHs2; lia. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)