proposition: Lemma weakening_ordertyping_app n Gamma Delta s A: Gamma ⊢(n) s : A -> Gamma ++ Delta ⊢(n) s : A.
proof: Proof. intros H; replace s with (ren id s) by now asimpl. eapply ordertyping_preservation_under_renaming; eauto. intros i B H'; unfold id. rewrite nth_error_app1; trivial. eapply nth_error_Some_lt; eauto. Qed.
imports: List Arith Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics typing)