proposition: Lemma freeVarsSuppAux2: 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. introv Hc. repnud Hc. exrepnd. pose proof (vFreshVarSpec ([v]++la ++ (tfreevars vc t)) v) as XX. remember (vFreshVar ([v]++la ++ tfreevars vc t) v) as vn. clear Heqvn. rw in_app_iff in XX. rw in_app_iff in XX. apply XX. right. left. apply Hc0. introv Hal. apply (ALtcase alpha_preserves_free_vars) in Hal. rewrite Hal in Hin. clear Hal. rewrite <- (tcase freevarsEquivariant) in Hin. rw in_map_iff in Hin. exrepnd. pose proof (swapVarInOrEq2 [(v,vn)] a) as Hs. rewrite <- Hin0 in Hs. clear Hin0. dimp Hs; simpl; cpx; [| constructor; auto| ]; cpx; repeat (disjoint_reasoning);cpx. introv Hc. dorn Hc; cpx. subst. clear Hs. apply XX. cpx. Qed.
imports: AlphaEquality SwapProps Eqdep_dec