proposition: Theorem AllButBindersSubset: forall {G : CFGV} {vc : VarSym G}, ( forall (s : GSym G) (nt : Term s), True) * ( forall (s : GSym G) (pt : Pattern s), subset (pAllButBinders vc pt ) (pAllVars pt) ) * ( forall (l : list (bool # GSym G)) (m : Mixture l), subset (mAllButBinders vc m) (mAllVars m) ).
proof: Proof. intros. GInduction; intros; cpx; allsimpl; eauto using subset_app_l, subset_app_r; apply app_subset; dands; eauto using subset_app_l, subset_app_r. Qed.
imports: CFGV Omega Eqdep_dec