proposition: Lemma albndDeepMakeAbPSubset : forall p (ma : Mixture (map (fun x : GSym G => (true, x)) (ppRhsSym p))), albindersDeep (MakeAbstractions vc ma []) = mBndngVarsDeep vc ma.
proof: Proof. introv. unfold MakeAbstractionsPNode. induction ma; allsimpl; auto; introv; apply app_if; autorewrite with fast; auto. Qed.
imports: Term AssociationList Swap AlphaEqProps SubstAux