proposition: Lemma ordertyping_completeness Gamma s A: Gamma ⊢ s : A -> exists n, Gamma ⊢(n) s : A.
proof: Proof. induction 1. - exists (ord A); eauto. - exists (ord (ctype X c)); eauto. - destruct IHtyping as [n]; exists (max (S (ord A)) n). econstructor; eauto. - destruct IHtyping1 as [n], IHtyping2 as [m]. exists (max n m); econstructor; eauto. Qed.
imports: List Arith Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics typing)