[STATEMENT]
lemma finite_Fvars_fmla[simp]:
  fixes A :: fmla
  shows "finite (Fvars A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (Fvars A)
[PROOF STEP]
by (induct A rule: fmla.induct) auto