proposition: Lemma alSSubstAux_MakeAbstractionsPNode : forall (p : PatProd G) (ma : Mixture (map (fun x : GSym G => (true, x)) (ppRhsSym p))) (sub : SSubstitution vc), alSSubstAux (MakeAbstractions vc ma []) sub = MakeAbstractions vc (mSSubstAux ma [] sub) [].
proof: Proof. induction ma; introv; allsimpl; auto; unfold SubFilter; try (rw ALFilter_nil_r); simpl; apply eq_cons; auto. Qed.
imports: Term AssociationList Swap AlphaEqProps SubstAux