proposition: Lemma inv_term_typing Gamma s A: Gamma ⊢(n) s : enc_type C A -> Gamma ⊢(n) inv_term C s : A.
proof: Proof. Proof using consts_agree O. intros H; unfold inv_term. eapply AppR_ordertyping with (L := map (ctype X) C). eapply const_ordertyping_list. rewrite O; auto. eapply ordertyping_preservation_consts; [auto|]. intros y ?; 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)