proposition: Lemma SSubstAuxSubFilter: ( (forall (s : GSym G) (t : Term s) (sub : SSubstitution vc) lf, disjoint (tfreevars vc t) lf -> tSSubstAux t sub = tSSubstAux t (SubFilter sub lf)) * (forall (s : GSym G) (pt : Pattern s) lf (sub : SSubstitution vc), disjoint (pfreevars vc pt) lf -> pSSubstAux pt sub = pSSubstAux pt (SubFilter sub lf)) * (forall (l : list (bool # GSym G)) (m : Mixture l) (llva : list (list (vType vc))) lf (sub : SSubstitution vc), disjoint (mfreevars vc m llva) lf -> mSSubstAux m llva sub = mSSubstAux m llva (SubFilter sub lf))).
proof: Proof. intros. apply GInduction; auto;[| | | | |]; try(intros; allsimpl; f_equal; apply H; auto);[ | | ]; try(introv Hp Hm Hdis; allsimpl; destruct llva; allsimpl; disjoint_reasoning;f_equal; auto;[]; unfold SubFilter; rw ALFilterSwap; rw <- ALFilterAppR; rw ALFilterAppAsDiff; rw ALFilterAppR; unfold subtractv in Hdis0; apply Hp; rw disjoint_diff_l in Hdis0; auto;fail);[]. - introv Hdis. simpl. rename vc0 into vcc. destruct_head_match; auto;[]. subst vcc. simpl. allunfold ALFindDef. remember (ALFind (DeqVtype vc) (SubFilter sub lf) v) as alf. destruct alf as [als | aln]. + applysym AssociationList.ALFindFilterSome in Heqalf. repnd. rw Heqalf0; auto. + applysym AssociationList.ALFindFilterNone in Heqalf. dorn Heqalf. * rw Heqalf; auto. * simpl in Hdis. rewrite DeqTrue in Hdis. simpl in Hdis. disjoint_reasoning. Qed.
imports: Term AssociationList