proposition: Theorem SSubstAuxNestSwap: ( forall (s : GSym G) (nt : Term s) (suba subb : SSubstitution vc) (H1dis: disjoint (tBndngVarsDeep vc nt) (rangeFreeVars suba ++ rangeFreeVars subb)) (H2dis: disjoint (rangeFreeVars suba) (ALDom subb)) (H3dis: disjoint (rangeFreeVars subb) (ALDom suba)) (H4dis: disjoint (ALDom suba) (ALDom subb)), tSSubstAux (tSSubstAux nt suba) subb = tSSubstAux (tSSubstAux nt subb) suba ) * ( forall (s : GSym G) (nt : Pattern s) (suba subb : SSubstitution vc) (H1dis: disjoint (pBndngVarsDeep vc nt) (rangeFreeVars suba ++ rangeFreeVars subb)) (H2dis: disjoint (rangeFreeVars suba) (ALDom subb)) (H3dis: disjoint (rangeFreeVars subb) (ALDom suba)) (H4dis: disjoint (ALDom suba) (ALDom subb)), pSSubstAux (pSSubstAux nt suba) subb = pSSubstAux (pSSubstAux nt subb) suba ) * ( forall (mp : MixtureParam) (nt : Mixture mp) (suba subb : SSubstitution vc) (llm : list (list (vType vc))) (H1dis: disjoint (mBndngVarsDeep vc nt ++ flatten llm) (rangeFreeVars suba ++ rangeFreeVars subb)) (H2dis: disjoint (rangeFreeVars suba) (ALDom subb)) (H3dis: disjoint (rangeFreeVars subb) (ALDom suba)) (H4dis: disjoint (ALDom suba) (ALDom subb)), mSSubstAux (mSSubstAux nt llm suba) llm subb = mSSubstAux (mSSubstAux nt llm subb) llm suba ).
proof: Proof. dands; intros; try disjoint_reasoning; allrw (tcase SSubstAuxNestAsApp); allrw (pcase SSubstAuxNestAsApp); allrw (mcase SSubstAuxNestAsApp); repeat disjoint_reasoning;[| |]; repeat (rw tSSubstAux_sub_trivial; try disjoint_reasoning); apply SSubstAuxAppAwap; trivial. Qed.
imports: Term AssociationList