have := propagateCarry_propagate f n
α β α' β'✝ : Type
γ δ : β → Type
β' : Type
f : (a : β) → δ a → β'
n : ℕ
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → α → Bool
init_carry_x : (a : β) → γ a → Bool
next_bit_x : (a : β) → (γ a → Bool) → (δ a → Bool) → (γ a → Bool) × Bool
x : β' → ℕ → Bool
⊢ propagateCarry init_carry next_bit (fun a => propagate (init_carry_x a) (next_bit_x a) fun d => x (f a d)) (n + 1) =
    propagateCarry (fun a => Sum.elim init_carry (fun b => init_carry_x b.fst b.snd) a)
        (fun carry bits =>
          let f := fun a => next_bit_x a (fun d => carry (inr { fst := a, snd := d })) fun d => bits (f a d);
          let g := next_bit (carry ∘ inl) fun a => (f a).snd;
          Sum.elim g fun x => Prod.fst (f x.fst) x.snd)
        x (n + 1) ∘
      inl
α β α' β'✝ : Type
γ δ : β → Type
β' : Type
f : (a : β) → δ a → β'
n : ℕ
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → α → Bool
init_carry_x : (a : β) → γ a → Bool
next_bit_x : (a : β) → (γ a → Bool) → (δ a → Bool) → (γ a → Bool) × Bool
x : β' → ℕ → Bool
this :
  ∀ (init_carry : α → Bool) (next_bit : (α → Bool) → (β → Bool) → α → Bool) (init_carry_x : (a : β) → γ a → Bool)
    (next_bit_x : (a : β) → (γ a → Bool) → (δ a → Bool) → (γ a → Bool) × Bool) (x : β' → ℕ → Bool),
    propagateCarry init_carry next_bit (fun a => propagate (init_carry_x a) (next_bit_x a) fun d => x (f a d)) n =
      propagateCarry (fun a => Sum.elim init_carry (fun b => init_carry_x b.fst b.snd) a)
          (fun carry bits =>
            let f := fun a => next_bit_x a (fun d => carry (inr { fst := a, snd := d })) fun d => bits (f a d);
            let g := next_bit (carry ∘ inl) fun a => (f a).snd;
            Sum.elim g fun x => Prod.fst (f x.fst) x.snd)
          x n ∘
        inl
⊢ propagateCarry init_carry next_bit (fun a => propagate (init_carry_x a) (next_bit_x a) fun d => x (f a d)) (n + 1) =
    propagateCarry (fun a => Sum.elim init_carry (fun b => init_carry_x b.fst b.snd) a)
        (fun carry bits =>
          let f := fun a => next_bit_x a (fun d => carry (inr { fst := a, snd := d })) fun d => bits (f a d);
          let g := next_bit (carry ∘ inl) fun a => (f a).snd;
          Sum.elim g fun x => Prod.fst (f x.fst) x.snd)
        x (n + 1) ∘
      inl