proposition: Lemma const_ordertyping_list Gamma n Cs: ord' (map (ctype X) Cs) <= S n -> Gamma ⊢₊(n) map const Cs : map (ctype X) Cs.
proof: Proof. induction Cs; cbn; (eauto 2). intros H; simplify in H; intuition; econstructor; (eauto 2). Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)