[GOAL]
n : ℕ
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
⊢ HEq (evenOddRec h0 h_even h_odd (bit false n)) (h_even n (evenOddRec h0 h_even h_odd n))
[PROOFSTEP]
rw [evenOddRec, binaryRec_eq]
[GOAL]
n : ℕ
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
⊢ HEq
    (match false, n,
      binaryRec h0
        (fun x x_1 x_2 =>
          match x, x_1, x_2 with
          | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
          | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
        n with
    | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
    | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
    (h_even n (evenOddRec h0 h_even h_odd n))
case h
n : ℕ
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
⊢ (match false, 0, h0 with
    | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
    | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi) =
    h0
[PROOFSTEP]
apply eq_rec_heq
[GOAL]
case h
n : ℕ
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
⊢ (match false, 0, h0 with
    | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
    | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi) =
    h0
[PROOFSTEP]
exact H
[GOAL]
n : ℕ
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
⊢ HEq (evenOddRec h0 h_even h_odd (bit true n)) (h_odd n (evenOddRec h0 h_even h_odd n))
[PROOFSTEP]
rw [evenOddRec, binaryRec_eq]
[GOAL]
n : ℕ
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
⊢ HEq
    (match true, n,
      binaryRec h0
        (fun x x_1 x_2 =>
          match x, x_1, x_2 with
          | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
          | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
        n with
    | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
    | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi)
    (h_odd n (evenOddRec h0 h_even h_odd n))
case h
n : ℕ
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
⊢ (match false, 0, h0 with
    | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
    | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi) =
    h0
[PROOFSTEP]
apply eq_rec_heq
[GOAL]
case h
n : ℕ
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
⊢ (match false, 0, h0 with
    | false, i, hi => (_ : 2 * i = bit0 i) ▸ h_even i hi
    | true, i, hi => (_ : 2 * i + 1 = bit1 i) ▸ h_odd i hi) =
    h0
[PROOFSTEP]
exact H
