induction xs
P : Formula
xs : List VarName
x : VarName
⊢ isFreeIn x (List.foldr forall_ P xs) ↔ x ∉ xs ∧ isFreeIn x P
case nil
P : Formula
x : VarName
⊢ isFreeIn x (List.foldr forall_ P []) ↔ x ∉ [] ∧ isFreeIn x P

case cons
P : Formula
x head✝ : VarName
tail✝ : List VarName
tail_ih✝ : isFreeIn x (List.foldr forall_ P tail✝) ↔ x ∉ tail✝ ∧ isFreeIn x P
⊢ isFreeIn x (List.foldr forall_ P (head✝ :: tail✝)) ↔ x ∉ head✝ :: tail✝ ∧ isFreeIn x P