proposition: Lemma SSubstAuxBVarsDisjoint: ( (forall (s : GSym G) (t : Term s) (sub : SSubstitution vc) lf, disjoint (tBndngVarsDeep vc t) lf -> disjoint (flat_map (tBndngVarsDeep vc) (ALRange sub)) lf -> disjoint (tBndngVarsDeep vc (tSSubstAux t sub)) lf) * (forall (s : GSym G) (pt : Pattern s) lf (sub : SSubstitution vc), disjoint (pBndngVarsDeep vc pt) lf -> disjoint (flat_map (tBndngVarsDeep vc) (ALRange sub)) lf -> disjoint (pBndngVarsDeep vc (pSSubstAux pt sub)) lf) * (forall (l : list (bool # GSym G)) (m : Mixture l) (llva : list (list (vType vc))) lf (sub : SSubstitution vc), disjoint (mBndngVarsDeep vc m) lf -> disjoint (flat_map (tBndngVarsDeep vc) (ALRange sub)) lf -> disjoint (mBndngVarsDeep vc (mSSubstAux m llva sub)) lf) ).
proof: Proof. intros. GInduction; cpx. - Case "vleaf". introv H1d H2d. allsimpl. ddeq; cpx. destruct e. simpl. unfold ALFindDef. dalfind; cpx. rw disjoint_flat_map_l in H2d. apply ALInEta in h0; cpx. - Case "mtcons". introv Hypt Hypm H1d H2d. allsimpl. destruct llva; allsimpl; cpx; repeat(disjoint_reasoning). apply Hypt; repeat(disjoint_reasoning). clear H1d H1d0. unfold SubFilter. SetReasoning. - Case "mpcons". introv Hypt Hypm H1d H2d. allsimpl. destruct llva; allsimpl; cpx; repeat(disjoint_reasoning). apply Hypt; repeat(disjoint_reasoning). clear H1d H1d0. unfold SubFilter. SetReasoning. Qed.
imports: Term AssociationList