fact: Fixpoint pAlreadyBndBinders {G : CFGV} {gs : GSym G} (vc : VarSym G) (pt : Pattern gs) {struct pt} : (list (vType vc)) := match pt with | ptleaf a v => [] | pvleaf vcc var => [] | pnode p lpt => mAlreadyBndBinders vc lpt | embed p nt => tBndngVarsDeep vc nt end with mAlreadyBndBinders {G : CFGV} {lgs : list (bool * GSym G)} (vc : VarSym G) (pts : Mixture lgs) {struct pts} : (list (vType vc)) := match pts with | mnil => [] | mtcons _ _ ph ptl => (tBndngVarsDeep vc ph) ++ (mAlreadyBndBinders vc ptl) | mpcons _ _ ph ptl => (pAlreadyBndBinders vc ph) ++ (mAlreadyBndBinders vc ptl) end.
imports: CFGV Omega