α : Type ?u.178408
β : Type ?u.178411
γ : Type ?u.178414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ succ One.toOfNat1.1 = { ofNat := ↑2 }.1
α : Type ?u.178408
β : Type ?u.178411
γ : Type ?u.178414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ succ 1 = 2
unfold instOfNat OfNat.ofNat
no goals
α : Type ?u.178408
β : Type ?u.178411
γ : Type ?u.178414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ succ One.toOfNat1.1 = { ofNat := ↑2 }.1
simpa using by rfl
no goals
α : Type ?u.178408
β : Type ?u.178411
γ : Type ?u.178414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ One.toOfNat1.1 = 1
rfl