[STATEMENT]
lemma term_variants_pred_inv_Var:
  "term_variants_pred P (Var x) t \<longleftrightarrow> t = Var x"
  "term_variants_pred P t (Var x) \<longleftrightarrow> t = Var x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. term_variants_pred P (Var x) t = (t = Var x) &&& term_variants_pred P t (Var x) = (t = Var x)
[PROOF STEP]
by (auto intro: term_variants_Var elim: term_variants_pred.cases)