proposition: Lemma vFreshVarSpec : forall {G : CFGV} {vc : VarSym G} (lvAvoid: list (vType vc)) (v: (vType vc)), ! LIn (vFreshVar lvAvoid v) lvAvoid.
proof: Proof. intros. unfold vFreshVar. revert v. revert lvAvoid. unfold vType. destruct (varSem G vc) as [T vd Vf Vfc]. allsimpl. exrepnd. allsimpl. cpx. Qed.
imports: GVariables