proposition: Lemma FreshDistRenWSpec: forall (VT : VarType) (lv :list (typ VT )) (lvAvoid :list (typ VT )), {lvn : list (typ VT ) $ no_repeats lvn # disjoint lvn lvAvoid # length lvn= length lv}.
proof: Proof. intros. eexists (ALRange (FreshDistinctRenamings VT lv lvAvoid)). pose proof (FreshDistRenSpec VT lv lvAvoid) as XX. allsimpl. exrepnd. apply (f_equal (@length _ )) in XX. allunfold ALDom. allunfold ALRange. autorewrite with fast. autorewrite with fast in XX. dands; cpx. Defined.
imports: AssociationList Omega