proposition: Lemma inj_typing n sigma Gamma Delta: Delta ⊩(n) sigma : Gamma -> Delta ⊩(n) sigma >> subst_consts inj : Gamma.
proof: Proof. Proof using consts_agree. intros ????. eapply ordertyping_preservation_consts; auto. intros ??; unfold inj. rewrite consts_agree. econstructor; rewrite <-consts_agree. eapply typing_constants; 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)