l : List Bool
b : Bool
this : (fun x => x == b) = fun a => decide ¬(a == !b) = true
⊢ countp (fun x => x == b) l = countp (fun a => decide ¬(a == !b) = true) l

case this
l : List Bool
b : Bool
⊢ (fun x => x == b) = fun a => decide ¬(a == !b) = true
l : List Bool
b : Bool
⊢ countp (fun x => x == b) l = countp (fun a => decide ¬(a == !b) = true) l
suffices : (fun x => x == b) = (fun a => decide ¬(a == !b) = true)
case this
l : List Bool
b : Bool
⊢ (fun x => x == b) = fun a => decide ¬(a == !b) = true
l : List Bool
b : Bool
this : (fun x => x == b) = fun a => decide ¬(a == !b) = true
⊢ countp (fun x => x == b) l = countp (fun a => decide ¬(a == !b) = true) l

case this
l : List Bool
b : Bool
⊢ (fun x => x == b) = fun a => decide ¬(a == !b) = true
rw [this]
case this.h
l : List Bool
b x : Bool
⊢ (x == b) = decide ¬(x == !b) = true
case this
l : List Bool
b : Bool
⊢ (fun x => x == b) = fun a => decide ¬(a == !b) = true
ext x
no goals
case this.h
l : List Bool
b x : Bool
⊢ (x == b) = decide ¬(x == !b) = true
cases x <;> cases b <;> rfl