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