proposition: Lemma eta₀_normal: normal (eta₀ s H₀).
proof: Proof. destruct eta₀_correct; eauto. Qed.
imports: Morphisms Setoid Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence typing order normalisation)