proposition: Lemma FreshDistVarsSpec: forall {G : CFGV} {vc : VarSym G} (lvAvoid: list (vType vc)) (lv: list (vType vc)), let lvn := (GFreshVars lvAvoid lv) in no_repeats lvn # disjoint lvn lvAvoid # length lvn= length lv.
proof: Proof. intros. subst lvn. unfold GFreshVars. pose proof( FreshDistVarsSpec lv lvAvoid). allsimpl. exrepnd; dands; cpx. Qed.
imports: GVariables