proposition: Lemma renBindersLBVLenSame : forall {G : CFGV} {vc : VarSym G} (l : list (bool # GSym G)) (pts : Mixture l) (lvA : lVars vc) (lln : list (list nat)), map (@length _) (lBoundVars vc lln pts) = map (@length _) (lBoundVars vc lln (mRenBinders lvA pts)).
proof: Proof. intros. apply lBoundVarsLenSameifNth. pose proof (@renBindersSameLength G vc). dands; cpx. Qed.
imports: AlphaEqProps Omega