case cons xs_hd xs_tl xs_ih =>
  simp
  simp only [isFreeIn]
  simp only [xs_ih]
  tauto
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isFreeIn x (List.foldr forall_ P xs_tl) ↔ x ∉ xs_tl ∧ isFreeIn x P
⊢ isFreeIn x (List.foldr forall_ P (xs_hd :: xs_tl)) ↔ x ∉ xs_hd :: xs_tl ∧ isFreeIn x P
no goals