fact: Fixpoint tSwap {G : CFGV} {vc : VarSym G} (gs : (GSym G)) (pt : Term gs) (sub : Swapping vc) {struct pt} : Term gs := match pt in Term gs return Term gs with | tleaf a b => tleaf a b | vleaf vcc var => vleaf vcc (match DeqVarSym vc vcc with | left eqq => swapVar (transport eqq sub) var | right _ => var end) | tnode p mix => tnode p (mSwap mix sub) end with pSwap {G : CFGV} {vc : VarSym G} {gs : GSym G} (pt : Pattern gs) (sub : Swapping vc) {struct pt} : Pattern gs := match pt with | ptleaf a v => ptleaf a v | pvleaf vcc var => pvleaf vcc (match DeqVarSym vc vcc with | left eqq => swapVar (transport eqq sub) var | right _ => var end) | pnode p lpt => pnode p (mSwap lpt sub) | embed p nt => embed p (tSwap nt sub) end with mSwap {G : CFGV} {vc : VarSym G} (lgs : list (bool * GSym G)) (pts : Mixture lgs) (sub : Swapping vc) {struct pts} : Mixture lgs := match pts in Mixture lgs return Mixture lgs with | mnil => mnil | mtcons _ _ ph ptl => mtcons (tSwap ph sub) (mSwap ptl sub) | mpcons _ _ ph ptl => mpcons (pSwap ph sub) (mSwap ptl sub) end.
imports: Term AssociationList