proposition: Lemma inv_subst_typing Delta sigma Gamma: Delta ⊩(n) sigma : enc_ctx C Gamma -> Delta ⊩(n) inv_subst C sigma : Gamma.
proof: Proof. Proof using consts_agree O. intros ????. eapply inv_term_typing, H. unfold enc_ctx; erewrite map_nth_error; auto. 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)