proposition: Lemma freeVarsSuppAux: 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. introv Hin. exists (tfreevars vc t). introv Hntal. destruct (in_deq _ (DeqVtype vc) a (tfreevars vc t)) as [ ? | Hneq]; cpx. provefalse. apply Hntal. apply (tcase alphaEqSwapNonFree). apply leavesLVarUnchanged1. allsimpl. repeat (disjoint_reasoning); cpx. Qed.
imports: AlphaEquality SwapProps Eqdep_dec