α : Type ?u.231373
β : Type ?u.231376
γ : Type ?u.231379
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c c' : Cardinal
h : ord c = ord c'
⊢ c = c'
α : Type ?u.231373
β : Type ?u.231376
γ : Type ?u.231379
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ Injective ord
intro c c' h
no goals
α : Type ?u.231373
β : Type ?u.231376
γ : Type ?u.231379
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c c' : Cardinal
h : ord c = ord c'
⊢ c = c'
rw [← card_ord c, ← card_ord c', h]