proposition: Lemma ordertyping_weak_preservation_under_renaming Gamma n s A delta Delta: Gamma ⊢(n) s : A -> (forall x A, nth Gamma x = Some A -> x ∈ vars s -> nth Delta (delta x) = Some A) -> Delta ⊢( n) ren delta s : A.
proof: Proof. induction s in delta, Gamma, Delta, A |-*; cbn -[vars]; intros; inv H; auto. - econstructor. eapply IHs; eauto. intros [] ? ?; cbn -[vars] in *; intuition auto. - econstructor; [eapply IHs1|eapply IHs2]; eauto. Qed.
imports: List Arith Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics typing)