proposition: Theorem SSubstAuxNestAsApp: ( forall (s : GSym G) (nt : Term s) (suba subb : SSubstitution vc) (Hdis: disjoint (tBndngVarsDeep vc nt) (rangeFreeVars suba)), tSSubstAux (tSSubstAux nt suba) subb = tSSubstAux nt (tSSubstAux_sub suba subb ++ subb) ) * ( forall (s : GSym G) (pt : Pattern s) (suba subb : SSubstitution vc) (Hdis: disjoint (pBndngVarsDeep vc pt) (rangeFreeVars suba)), pSSubstAux (pSSubstAux pt suba) subb = pSSubstAux pt (tSSubstAux_sub suba subb ++ subb) ) * ( forall (l : list (bool # GSym G)) (m : Mixture l) (suba subb : SSubstitution vc) (llm : list (list (vType vc))) (Hdis: disjoint (mBndngVarsDeep vc m ++ (flatten llm)) (rangeFreeVars suba)), mSSubstAux (mSSubstAux m llm suba) llm subb = mSSubstAux m llm ((tSSubstAux_sub suba subb) ++ subb) ).
proof: Proof. GInduction; allsimpl; introns Hyp; intros; allsimpl; cpx; try (f_equal;cpx;fail); allsimpl; repeat (disjoint_reasoning); [| | | |]. - Case "vleaf". simpl. rename vc0 into vcc; allsimpl; destruct_head_match; auto;simpl; [|destruct_head_match;cpx; fail]. rename e into Heq. revert v. rw <- Heq. intros. simpl. DALFind a1l;[|];symmetry in Heqa1l. + apply ALFindRangeMapSome with (f:=(fun t => tSSubstAux t subb)) in Heqa1l. rw ALFindApp. unfold tSSubstAux_sub. rw Heqa1l; cpx. + apply ALFindRangeMapNone with (f:=(fun t => tSSubstAux t subb)) in Heqa1l. rw ALFindApp. unfold tSSubstAux_sub. rw Heqa1l; simpl; cpx. rewrite DeqTrue. cpx. - Case "tnode". f_equal. rw <- lBoundVarsSameSSubstAux. apply Hyp. repeat(disjoint_reasoning);[]. SetReasoning. - Case "pnode". f_equal. apply Hyp. repeat(disjoint_reasoning);[]. SetReasoning. - Case "mtcons". destruct llm as [| lh llm];allsimpl;f_equal; try apply Hyp; try apply Hyp0; repeat(disjoint_reasoning); SetReasoning;[]. unfold SubFilter. rw ALFilterAppSub. unfold tSSubstAux_sub. rw ALMapRangeFilterCommute. rw <- tSSubstAuxSubUnfold. rewrite <- tSSubstAuxSubFilter with (lv:=lh); repeat(disjoint_reasoning); SetReasoning. apply Hyp. repeat(disjoint_reasoning); SetReasoning. - Case "mpcons". destruct llm as [| lh llm];allsimpl;f_equal; try apply Hyp; try apply Hyp0; repeat(disjoint_reasoning); SetReasoning;[]. unfold SubFilter. rw ALFilterAppSub. unfold tSSubstAux_sub. rw ALMapRangeFilterCommute. rw <- tSSubstAuxSubUnfold. rewrite <- tSSubstAuxSubFilter with (lv:=lh); repeat(disjoint_reasoning); SetReasoning. apply Hyp. repeat(disjoint_reasoning); SetReasoning. Qed.
imports: Term AssociationList