proposition: Lemma ordertypingSubst_complete Delta sigma Gamma: Delta ⊩ sigma : Gamma -> exists n, Delta ⊩(n) sigma : Gamma.
proof: Proof. induction Gamma as [| A Gamma IH] in sigma |-* . - intros _. exists 0. intros []?; cbn; discriminate. - intros ?. specialize (IH (shift >> sigma)). mp IH; [intros ???; eauto|]. specialize (H 0 A); mp H; eauto. eapply ordertyping_completeness in H. destruct IH as [n], H as [m]. exists (max n m); intros [|x]B; cbn; [injection 1 as ->|intros]. all: eapply ordertyping_monotone. 2, 4: eauto. all: eauto. Qed.
imports: List Arith Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics typing)