proposition: Lemma remove_constants_ordertypingSubst Delta sigma Gamma : Delta ⊩(n) sigma : Gamma -> (forall x c, c ∈ consts (sigma x) -> R' c = None -> c ∈ C) -> enc_ctx C Delta ⊩(n) enc_subst C sigma : enc_ctx C Gamma.
proof: Proof. Proof using consts_agree O. intros ?????. unfold enc_ctx in H1. rewrite nth_error_map_option in H1. destruct nth eqn: EQ; try discriminate; injection H1 as <-. eapply remove_constants_ordertyping; 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)