no goals
α : Type ?u.182364
β : Type ?u.182367
γ : Type ?u.182370
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
⊢ card (succ o) = card o + 1
simp only [← add_one_eq_succ, card_add, card_one]