proposition: Lemma albndDeepMakeAbTSubset : forall (p : TermProd G) (ma : Mixture (tpRhsAugIsPat p)), subset (albindersDeep (MakeAbstractions vc ma (lBoundVars vc (bndngPatIndices p) ma))) (mBndngVarsDeep vc ma).
proof: Proof. introv. unfold MakeAbstractionsTNode, MakeAbstractionsTNodeAux. pose proof (@lBoundVarsmBndngVars _ vc _ ma (bndngPatIndices p)) as Hs. pose proof (lBoundVarsLength vc ma (bndngPatIndices p)) as Hl. remember ((lBoundVars vc (bndngPatIndices p) ma)) as llb. eapply subset_trans;[apply subsetAlbindersDeep|]. apply subset_app. dands; eauto. eauto 2 with SetReasoning. Qed.
imports: Term AssociationList Swap AlphaEqProps SubstAux