no goals
α : Type ?u.85057
β : Type ?u.85060
γ : Type ?u.85063
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
x✝ : ∃ a, o = succ a
a : Ordinal
e : o = succ a
⊢ succ (pred o) = o
simp only [e, pred_succ]