α : Type ?u.179670
⊢ (match (motive := Bool → Num → Num) true with
      | true => Num.bit1
      | false => Num.bit0)
      0 =
    1
α : Type ?u.179670
⊢ ofNat' 1 = 1
erw [ofNat'_bit true 0, cond, ofNat'_zero]
no goals
α : Type ?u.179670
⊢ (match (motive := Bool → Num → Num) true with
      | true => Num.bit1
      | false => Num.bit0)
      0 =
    1
rfl