proposition: Lemma eqSetDeepShallowPlusAlready: forall {G : CFGV} {vc : VarSym G}, ( forall (s : GSym G) (nt : Term s), True) * ( forall (s : GSym G) (pt : Pattern s), eqset (pBndngVarsDeep vc pt ) (pBndngVars vc pt ++ pAlreadyBndBinders vc pt) ) * ( forall (l : list (bool # GSym G)) (m : Mixture l), eqset (mBndngVarsDeep vc m) (mBndngVars vc m ++ mAlreadyBndBinders vc m) ).
proof: Proof. intros. GInduction; intros; cpx. - Case "pvleaf". simpl; ddeq; cpx. - Case "mtcons". allsimpl. eapply eqset_trans;[|apply eqsetCommute]. rw <- app_assoc. apply eqset_app_if; cpx. eapply eqset_trans;[|apply eqsetCommute]; cpx. - Case "mpcons". allsimpl. eapply eqset_trans;[|apply eqsetCommute3]. rw <- app_assoc. rw app_assoc. apply eqset_app_if; cpx. eapply eqset_trans;[|apply eqsetCommute]. cpx. Qed.
imports: CFGV Omega Eqdep_dec