proposition: Theorem SSubstAuxAppAwap: ( forall (s : GSym G) (nt : Term s) (suba subb : SSubstitution vc) (Hdis : disjoint (ALDom suba) (ALDom subb)), (tSSubstAux nt (suba ++ subb)) = (tSSubstAux nt (subb ++ suba)) ) * ( forall (s : GSym G) (pt : Pattern s) (suba subb : SSubstitution vc) (Hdis : disjoint (ALDom suba) (ALDom subb)), (pSSubstAux pt (suba ++ subb)) = (pSSubstAux pt (subb ++ suba)) ) * ( forall (l : list (bool # GSym G)) (m : Mixture l) (lln : list (list (vType vc))) (suba subb : SSubstitution vc) (Hdis : disjoint (ALDom suba) (ALDom subb)), (mSSubstAux m lln (suba ++ subb)) = (mSSubstAux m lln (subb ++ suba)) ).
proof: Proof. GInduction; allsimpl; introns Hyp; intros; allsimpl; cpx; try (f_equal; auto);[| |]. - Case "vleaf". simpl. rename vc0 into vcc. destruct_head_match; auto;[]. subst vcc. simpl. allunfold ALFindDef. allrw ALFindApp. DALFind a1l; DALFind a2l; cpx;[]. allapplysym ALFindSome. allapply ALInEta; exrepnd. disjoint_lin_contra. - Case "mtcons". destruct lln; allsimpl; f_equal; cpx. unfold SubFilter. allrw ALFilterAppSub. apply Hyp; cpx. apply (subset_disjointLR Hyp1); SetReasoning. - Case "mpcons". destruct lln; allsimpl; f_equal; cpx. unfold SubFilter. allrw ALFilterAppSub. apply Hyp; cpx. apply (subset_disjointLR Hyp1); SetReasoning. Qed.
imports: Term AssociationList