simp only [isFreeIn]
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 (forall_ xs_hd (List.foldr forall_ P xs_tl)) ↔ (¬x = xs_hd ∧ x ∉ xs_tl) ∧ isFreeIn x P
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
⊢ ¬x = xs_hd ∧ isFreeIn x (List.foldr forall_ P xs_tl) ↔ (¬x = xs_hd ∧ x ∉ xs_tl) ∧ isFreeIn x P