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