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