no goals
α : Type ?u.163687
r : α → α → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
ho : card o < c
hc' : c ≠ ℵ₀
hf : ∀ (i : Ordinal) (hi : i < o) (b : Ordinal), b < ord c → f i hi b < ord c
a : Ordinal
⊢ lift (card o) < c
rwa [lift_id]