proposition: Lemma subst_consts_up Y Z (zeta: Y -> exp Z) (sigma: fin -> exp Y): up (sigma >> subst_consts zeta) = up sigma >> subst_consts (zeta >> ren shift).
proof: Proof. fext; intros []; cbn; trivial. unfold funcomp at 1 2. now rewrite <-ren_subst_consts_commute. Qed.
imports: Morphisms Lia List Undecidability.HOU(calculus.calculus)