proposition: Lemma GFreshDistRenWSpec: forall {G:CFGV} (vc : VarSym G) (lv :list (vType vc)) (lvAvoid :list (vType vc)), {lvn : list (vType vc) $ no_repeats lvn # disjoint lvn lvAvoid # length lvn= length lv}.
proof: Proof. intros. eapply FreshDistRenWSpec; eauto. Defined.
imports: GVariables