proposition: Lemma bindersDeep_in_allvars : forall {G : CFGV} {vc : VarSym G}, ( (forall (gs : GSym G) (t : Term gs), subset (tBndngVarsDeep vc t) (tAllVars t)) * (forall (gs : GSym G) (p : Pattern gs), subset (pBndngVarsDeep vc p) (pAllVars p)) * (forall (lgs : list (bool * GSym G)) (m : Mixture lgs), subset (mBndngVarsDeep vc m) (mAllVars m)) ).
proof: Proof. intros. GInduction; auto; introv; try (complete (allsimpl; cpx)); try (complete (allsimpl; introv f e; DDeqs; cpx)). - Case "mtcons". allsimpl. introv T M; introv i. allrw in_app_iff; sp. - Case "mpcons". allsimpl. introv P M; introv i. allrw in_app_iff; sp. Qed.
imports: CFGV Omega Eqdep_dec