proposition: Lemma RenBindersSpec2 : forall {G : CFGV} (vc : VarSym G), ( forall (s : GSym G) (nt : Term s), True) * ( forall (s : GSym G) (pt : Pattern s) (lvAvoid : lVars vc), pAlreadyBndBinders vc pt = pAlreadyBndBinders vc (pRenBinders lvAvoid pt) ) * ( forall (l : list (bool # GSym G)) (m : Mixture l) (lvAvoid : lVars vc), mAlreadyBndBinders vc m = mAlreadyBndBinders vc (mRenBinders lvAvoid m) ).
proof: Proof. intros; GInduction; allsimpl; cpx;[|]; intros; f_equal; cpx. Qed.
imports: AlphaEqProps Omega