tauto
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isBoundIn x (List.foldr forall_ P xs_tl) ↔ x ∈ xs_tl ∨ isBoundIn x P
⊢ x = xs_hd ∨ x ∈ xs_tl ∨ isBoundIn x P ↔ (x = xs_hd ∨ x ∈ xs_tl) ∨ isBoundIn x P
no goals