proposition: Lemma ordertyping_weak_preservation_under_substitution n sigma Gamma Delta s A: Gamma ⊢(n) s : A -> (forall i A, i ∈ vars s -> nth Gamma i = Some A -> Delta ⊢(n) sigma i : A) -> Delta ⊢(n) sigma • s : A.
proof: Proof. induction 1 in sigma, Delta |-*; intros H'; cbn [subst_exp]; subst; auto. - econstructor; auto; eapply IHordertyping. intros [|m]; cbn; trivial. + intros ? H1; injection 1 as <-; econstructor; cbn; trivial. eapply vars_ordertyping in H1 as []; eauto. intuition idtac. now injection H1 as ->. + intros D H1 H2; unfold funcomp. eapply ordertyping_preservation_under_renaming; auto. now intros i. - econstructor; [eapply IHordertyping1 | eapply IHordertyping2]. all: intros; eapply H'; eauto. Qed.
imports: List Arith Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics typing)