proposition: Lemma eta₀_typing: Gamma ⊢(n) eta₀ s H₀ : A.
proof: Proof. eapply ordertyping_preservation_under_steps. rewrite <-eta₀_correct. all: eauto. Qed.
imports: Morphisms Setoid Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence typing order normalisation)