proposition: Lemma fresh_vars : forall (n: nat) (lv : list NVar), {lvn : (list NVar) & no_repeats lvn # disjoint lvn lv # length lvn = n}.
proof: Proof. intros. exists (fresh_distinct_vars n lv). apply fresh_distinct_vars_spec. Qed.
imports: list Omega