fact: Definition eta₀ (s: exp X) {Gamma n A} (H: Gamma ⊢(n) s : A) := proj1_sig (compute_evaluation_step (ordertyping_termination_steps H)).
imports: Morphisms Setoid Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence typing order normalisation)