. rfl
case zero
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
x : β' → ℕ → Bool
changeVars : β → β'
⊢ propagate init_carry next_bit (fun b => x (changeVars b)) Nat.zero =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x Nat.zero

case succ
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
x : β' → ℕ → Bool
changeVars : β → β'
i : ℕ
ih :
  propagate init_carry next_bit (fun b => x (changeVars b)) i =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x i
⊢ propagate init_carry next_bit (fun b => x (changeVars b)) (Nat.succ i) =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x (Nat.succ i)
case succ
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
x : β' → ℕ → Bool
changeVars : β → β'
i : ℕ
ih :
  propagate init_carry next_bit (fun b => x (changeVars b)) i =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x i
⊢ propagate init_carry next_bit (fun b => x (changeVars b)) (Nat.succ i) =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x (Nat.succ i)