proposition: Lemma FreshDistVarsSpec: forall {T : VarType} (lv :list (typ T)) (lvAvoid :list (typ T)), let lvn := (FreshDistinctVars T lv lvAvoid) in no_repeats lvn # disjoint lvn lvAvoid # length lvn= length lv.
proof: Proof. induction lv as [| h tl Hind]; intros; subst lvn; [dands; cpx|]. allsimpl. destruct T. allsimpl. exrepnd. allsimpl. specialize (Hind ((fresh0 lvAvoid [h]):: lvAvoid)). repnd; allsimpl. dands; try econstructor; eauto; try congruence. - apply disjoint_sym in Hind1. apply Hind1; cpx. - repeat (disjoint_reasoning). Defined.
imports: AssociationList Omega