no goals
α : Type ?u.110267
β : Type ?u.110270
γ : Type ?u.110273
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
H : IsNormal f
a b : Ordinal
⊢ f a = f b ↔ a = b
simp only [le_antisymm_iff, H.le_iff]