proposition: Lemma mRenBindersSpec3 : forall {G : CFGV} {vc : VarSym G} {mp : MixtureParam} (pts : Mixture mp) (lln : list (list nat)) (lvAvoid : list (vType vc)), validBsl (length mp) lln -> lForall no_repeats (lBoundVars vc lln (mRenBinders (lvAvoid) pts)).
proof: Proof. intros. pose proof ((mcase (RenBindersSpec vc)) _ pts lvAvoid) as Hs. simpl in Hs. repnd. rewrite mBndngVarsAsNth in Hs0. clear Hs. rw (@lForallSame (list (vType vc))). unfold lBoundVars. introv Hin. apply in_map_iff in Hin. exrepnd. subst. rename a0 into ln. apply X in Hin1. repnud Hin1. induction ln; cpx. allrw no_repeats_cons. allsimpl. repnd. apply IHln in Hin2; cpx;[]. clear IHln. allrw no_repeats_app. dands;cpx. - apply no_rep_flat_map_seq1 with (n:=0) (len := length mp); sp. apply LInSeqIff; dands; omega. - intros. introv Hin Hinc. apply lin_flat_map in Hinc. exrepnd. destruct (deq_nat x a); subst; cpx. eapply no_rep_flat_map_seq2 in n; eauto. + disjoint_lin_contra. + rw (@lForallSame nat) in Hin1. apply Hin1 in Hinc1. apply LInSeqIff; dands; omega. + apply LInSeqIff; dands; omega. Qed.
imports: AlphaEqProps Omega