fact: Fixpoint tSSubstAux {G : CFGV} {vc : VarSym G} (gs : (GSym G)) (pt : Term gs) (sub : SSubstitution vc) {struct pt} : Term gs := match pt in Term gs return Term gs with | tleaf a b => tleaf a b | vleaf vcc var => match DeqVarSym vc vcc with | left eqq => ALFindDef (DeqVtype vcc) (transport eqq sub) var (vleaf vcc var) | right _ => (vleaf vcc var) end | tnode p mix => tnode p (mSSubstAux mix (lBoundVars vc (bndngPatIndices p ) mix) sub) end with pSSubstAux {G : CFGV} {vc : VarSym G} {gs : (GSym G)} (pt : Pattern gs) (sub : SSubstitution vc) {struct pt} : Pattern gs := match pt with | ptleaf a v => ptleaf a v | pvleaf vcc var => pvleaf vcc var | pnode p lpt => pnode p (mSSubstAux lpt [] sub) | embed p nt => embed p (tSSubstAux nt sub) end with mSSubstAux {G : CFGV} {vc : VarSym G} (lgs : list (bool * GSym G)) (pts : Mixture lgs) (lbvars : list (list (vType vc))) (sub : SSubstitution vc) {struct pts} : Mixture lgs := match pts in Mixture lgs return Mixture lgs with | mnil => mnil | mtcons _ _ ph ptl => match lbvars with | [] => mtcons (tSSubstAux ph sub) (mSSubstAux ptl [] sub) | lh ::ltl => mtcons (tSSubstAux ph (SubFilter sub lh)) (mSSubstAux ptl ltl sub) end | mpcons _ _ ph ptl => match lbvars with | [] => mpcons (pSSubstAux ph sub) (mSSubstAux ptl [] sub) | lh ::ltl => mpcons (pSSubstAux ph (SubFilter sub lh)) (mSSubstAux ptl ltl sub) end end.
imports: Term AssociationList