funext i
case h.succ.e_x
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
n✝ : ℕ
⊢ x = fun b => bif b then x true else x false
case h.succ.e_x.h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
n✝ : ℕ
i : Bool
⊢ x i = bif i then x true else x false