proposition: Lemma repeated_ordertyping n Gamma S A: (forall s, s ∈ S -> Gamma ⊢(n) s : A) -> forall m, m = length S -> Gamma ⊢₊(n) S : repeat A m.
proof: Proof. induction S; cbn; intros; subst; cbn; (eauto 2). intuition. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)