no goals
α : Type ?u.315442
β : Type ?u.315445
γ : Type ?u.315448
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : (a : Ordinal) → a < 1 → Ordinal
⊢ bsup 1 f = f 0 (_ : 0 < 1)
simp_rw [← sup_eq_bsup, sup_unique, familyOfBFamily, familyOfBFamily', typein_one_out]