fact: Fixpoint pSwapEmbed {G : CFGV} {vc : VarSym G} {gs : GSym G} (pt : Pattern gs) (swEmbed : Swapping 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 (mSwapEmbed lpt swEmbed) | embed p nt => embed p (tSwap nt swEmbed) end with mSwapEmbed {G : CFGV} {vc : VarSym G} {lgs : list (bool * GSym G)} (pts : Mixture lgs) (swEmbed : Swapping vc) {struct pts} : Mixture lgs := match pts in Mixture lgs return Mixture lgs with | mnil => mnil | mtcons _ _ ph ptl => mtcons ph (mSwapEmbed ptl swEmbed) | mpcons _ _ ph ptl => mpcons (pSwapEmbed ph swEmbed) (mSwapEmbed ptl swEmbed) end.
imports: Term AssociationList