cases b
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
b : ℕ
⊢ propagate (fun x => false)
      (fun carry bits =>
        (fun x => bits true && bits false || bits false && carry () || bits true && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      x b =
    propagate (fun x => false)
      (fun carry bits =>
        (fun x => bits true && bits false || bits false && carry () || bits true && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      (fun b => bif b then x true else x false) b
case h.zero
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
⊢ propagate (fun x => false)
      (fun carry bits =>
        (fun x => bits true && bits false || bits false && carry () || bits true && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      x Nat.zero =
    propagate (fun x => false)
      (fun carry bits =>
        (fun x => bits true && bits false || bits false && carry () || bits true && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      (fun b => bif b then x true else x false) Nat.zero

case h.succ
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
n✝ : ℕ
⊢ propagate (fun x => false)
      (fun carry bits =>
        (fun x => bits true && bits false || bits false && carry () || bits true && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      x (Nat.succ n✝) =
    propagate (fun x => false)
      (fun carry bits =>
        (fun x => bits true && bits false || bits false && carry () || bits true && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      (fun b => bif b then x true else x false) (Nat.succ n✝)