fact: Record VarType := { typ : Type; eqdec : Deq typ; fresh : forall (avoid : list typ) (sugg : list typ),typ; freshCorrect: forall (avoid : list typ) (sugg : list typ), !(LIn (fresh avoid sugg) avoid) }.
imports: AssociationList Omega