no goals
α : Type ?u.187136
β : Type ?u.187139
γ : Type ?u.187142
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
x : (Quotient.out 1).α
⊢ typein (fun x x_1 => x < x_1) x = 0
rw [one_out_eq x, typein_enum]