proposition: Lemma re_typing n Delta f sigma Gamma: 1 <= n -> Delta ⊩(n) sigma : Gamma -> (forall x c, x ∈ dom Gamma -> c ∈ consts (sigma x) -> nth Delta (f c) = Some (target (ctype Y c))) -> Delta ⊩(n) sigma >> subst_consts (re f) : Gamma.
proof: Proof. Proof using consts_agree. intros L T Sub x A H; unfold funcomp. eapply ordertyping_preservation_consts; auto. intros y H'. unfold re. destruct (tight RE y) eqn: EQr. - eapply tight_is_tight in EQr. subst. rewrite <-consts_agree. econstructor. rewrite consts_agree. eapply typing_constants; eauto. - eapply ordertyping_monotone, inhab_typing; domin H; eauto. Qed.
imports: List Arith Lia Morphisms Setoid Undecidability.HOU(calculus.calculus) Undecidability.HOU(unification.higher_order_unification unification.nth_order_unification concon.conservativity_constants concon.conservativity)