proposition: Lemma FreshDistRenSpec: forall (VT : VarType) (lv :list (typ VT )) (lvAvoid :list (typ VT )), let sw := (FreshDistinctRenamings VT lv lvAvoid) in no_repeats (ALRange sw) # disjoint (ALRange sw) lvAvoid # ALDom sw = lv.
proof: Proof. induction lv as [| h tl Hind]; intros; [dands; cpx|]. allsimpl. destruct VT; 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