ext b
case h.e__bits
α β α' β'✝ : 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
a : α
⊢ (fun i =>
      (next_bit_x i (propagateCarry (init_carry_x i) (fun c b => (next_bit_x i c b).fst) (fun d => x (f i d)) n)
          fun j => x (f i j) (n + 1)).snd) =
    fun a =>
    (next_bit_x a
        (fun d =>
          propagateCarry (fun a => Sum.elim init_carry (fun b => init_carry_x b.fst b.snd) a)
            (fun carry bits =>
              Sum.elim
                (next_bit (carry ∘ inl) fun a =>
                  (next_bit_x a (fun d => carry (inr { fst := a, snd := d })) fun d => bits (f a d)).snd)
                fun x =>
                Prod.fst (next_bit_x x.fst (fun d => carry (inr { fst := x.fst, snd := d })) fun d => bits (f x.fst d))
                  x.snd)
            x n (inr { fst := a, snd := d }))
        fun d => x (f a d) (n + 1)).snd
case h.e__bits.h
α β α' β'✝ : 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
a : α
b : β
⊢ (next_bit_x b (propagateCarry (init_carry_x b) (fun c b_1 => (next_bit_x b c b_1).fst) (fun d => x (f b d)) n)
        fun j => x (f b j) (n + 1)).snd =
    (next_bit_x b
        (fun d =>
          propagateCarry (fun a => Sum.elim init_carry (fun b => init_carry_x b.fst b.snd) a)
            (fun carry bits =>
              Sum.elim
                (next_bit (carry ∘ inl) fun a =>
                  (next_bit_x a (fun d => carry (inr { fst := a, snd := d })) fun d => bits (f a d)).snd)
                fun x =>
                Prod.fst (next_bit_x x.fst (fun d => carry (inr { fst := x.fst, snd := d })) fun d => bits (f x.fst d))
                  x.snd)
            x n (inr { fst := b, snd := d }))
        fun d => x (f b d) (n + 1)).snd