fact: Fixpoint pRenBinders {G : CFGV} { vc : VarSym G} {gs : (GSym G)} (lvAvoid : lVars vc) (p : Pattern gs) {struct p} : Pattern gs := match p in Pattern gs return Pattern gs with | ptleaf tc t => ptleaf tc t | pvleaf vcc var => pvleaf vcc (match (DeqVarSym vc vcc) with | left eqq => (vFreshVar (transport eqq lvAvoid) var) | right _ => var end) | pnode p mix => pnode p (mRenBinders lvAvoid mix) | embed p t => embed p t end with mRenBinders {G : CFGV} { vc : VarSym G} {lgs : list (bool * GSym G)} (lvAvoid : list (vType vc)) (pts : Mixture lgs) {struct pts} : Mixture lgs := match pts with | mnil => mnil | mtcons _ _ ph ptl => mtcons ph (mRenBinders lvAvoid ptl) | mpcons _ _ ph ptl => let phr := (pRenBinders lvAvoid ph) in let phrb := pBndngVars vc phr in mpcons phr (mRenBinders (lvAvoid ++ phrb) ptl) end.
imports: AlphaEqProps Omega