proposition: Lemma freeVarsSupp: forall {G : CFGV} {vc : VarSym G}, ((forall (s : GSym G) (t : Term s), forall v, LIn v (tfreevars vc t) <=> !(finite (fun b => !(tAlphaEq vc t (tSwap t [(v,b)])))))).
proof: Proof. intros. split. - apply freeVarsSuppAux2. - introv Hin. destruct (in_deq _ (DeqVtype vc) v (tfreevars vc t)) as [ ? | Hneq]; cpx. provefalse. apply Hin. apply freeVarsSuppAux. trivial. Qed.
imports: AlphaEquality SwapProps Eqdep_dec