fact: Fixpoint tRenAlpha {G : CFGV} {vc : VarSym G} {gs : (GSym G)} (pt : Term gs) (lvAvoid : list (vType 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 var | tnode p mix => tnode p ( let rmix := mRenAlpha mix lvAvoid in nodeRenAlphaAux (bndngPatIndices p) rmix lvAvoid ) end with pRenAlpha {G : CFGV} {vc : VarSym G} {gs : (GSym G)} (pt : Pattern gs) (lvAvoid : list (vType 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 (mRenAlpha lpt lvAvoid) | embed p nt => embed p (tRenAlpha nt lvAvoid) end with mRenAlpha {G : CFGV} {vc : VarSym G} {lgs : list (bool * GSym G)} (pts : Mixture lgs) (lvAvoid : list (vType vc)) {struct pts} : Mixture lgs := match pts in Mixture lgs return Mixture lgs with | mnil => mnil | mtcons _ _ th ttl => mtcons (tRenAlpha th lvAvoid) (mRenAlpha ttl lvAvoid) | mpcons _ _ ph ptl => mpcons (pRenAlpha ph lvAvoid) (mRenAlpha ptl lvAvoid) end.
imports: AlphaEqProps Omega