proposition: Lemma ordertyping_preservation_consts X Y n Gamma s A (zeta: X -> exp Y): Gamma ⊢(n) s : A -> (forall x, x ∈ consts s -> Gamma ⊢(n) zeta x : ctype X x) -> Gamma ⊢(n) subst_consts zeta s : A.
proof: Proof. induction 1 in zeta |-*; cbn; [eauto|eauto|..]. - intros H'. econstructor. eapply IHordertyping. intros; eapply ordertyping_preservation_under_renaming; [eauto|]. intros ?; cbn; eauto. - intros H'. econstructor. eapply IHordertyping1; intros ??; eapply H'; simplify; intuition idtac. eapply IHordertyping2; intros ??; eapply H'; simplify; intuition idtac. Qed.
imports: Morphisms Lia List Undecidability.HOU(calculus.calculus)