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