proposition: Lemma ordertyping_preservation_under_reduction n s s' Gamma A: s > s' -> Gamma ⊢(n) s : A -> Gamma ⊢(n) s' : A.
proof: Proof. induction 1 in n, Gamma, A |-*; intros H1; invp @ordertyping; eauto. inv H3. eapply ordertyping_weak_preservation_under_substitution; eauto. intros []; cbn; trivial. intros ? _; now injection 1 as ->. intros D H6 H7. eapply vars_ordertyping in H6 as [B]; eauto. intuition. econstructor; intuition idtac. cbn in H0; rewrite H0 in H7; now injection H7 as ->. Qed.
imports: List Arith Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics typing)