proposition: Lemma subst_const_comm {X Y} (zeta: X -> exp Y) sigma delta s: (forall x, sigma (delta x) = var x) -> subst_consts zeta (sigma • s) = (sigma >> subst_consts zeta) • (subst_consts (zeta >> ren delta) s).
proof: Proof. induction s in zeta, sigma, delta |-*; intros H; cbn. - reflexivity. - unfold funcomp; asimpl. rewrite idSubst_exp; trivial. intros y; unfold funcomp; cbn. rewrite H; reflexivity. - f_equal. erewrite IHs with (delta := 0 .: delta >> shift). 2: intros []; cbn; unfold funcomp; trivial; rewrite H; reflexivity. f_equal; [| now asimpl]. fext; intros []; cbn; trivial. unfold funcomp at 2. now rewrite ren_subst_consts_commute. - erewrite IHs1, IHs2; eauto. Qed.
imports: Morphisms Lia List Undecidability.HOU(calculus.calculus)