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