proposition: Lemma ordertyping_normalise_subst sigma Delta : Delta ⊩(n) sigma : Gamma -> {tau | (forall x : fin, sigma x >* tau x) /\ (forall x : nat, x ∈ dom Gamma -> normal (tau x)) /\ Delta ⊩(n) tau : Gamma}.
proof: Proof. intros H; eapply ordertypingSubst_soundness in H as H'; eapply normalise_subst in H' as [tau]. exists tau; intuition idtac. intros ???. eapply ordertyping_preservation_under_steps; [eapply H0 |]. eapply H; eauto. Qed.
imports: List Lia Morphisms Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification unification.systemunification)