proposition: Lemma disjointDeepShallowPlusAlready: forall {G : CFGV} {vc : VarSym G} (l : list (bool # GSym G)) (m : Mixture l) lva, disjoint (mBndngVars vc m ++ mAlreadyBndBinders vc m) lva -> disjoint (mBndngVarsDeep vc m) lva.
proof: Proof. introv Hdis. SetReasoning. apply eqsetSubset. apply eqset_sym. apply eqSetDeepShallowPlusAlready. Qed.
imports: CFGV Omega Eqdep_dec