C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
⊢ (if n0 : 0 = 0 then Eq.mpr (_ : C 0 = C 0) z
    else
      let n' := div2 0;
      let_fun _x := (_ : bit (bodd 0) (div2 0) = 0);
      Eq.mpr (_ : C 0 = C (bit (bodd 0) n')) (f (bodd 0) n' (binaryRec z f n'))) =
    z
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
⊢ binaryRec z f 0 = z
rw [binaryRec]
no goals
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
⊢ (if n0 : 0 = 0 then Eq.mpr (_ : C 0 = C 0) z
    else
      let n' := div2 0;
      let_fun _x := (_ : bit (bodd 0) (div2 0) = 0);
      Eq.mpr (_ : C 0 = C (bit (bodd 0) n')) (f (bodd 0) n' (binaryRec z f n'))) =
    z
rfl