fact: Fixpoint tAllVars {G : CFGV} { vc : VarSym G} {gs : (GSym G)} (t : Term gs) {struct t} : (list (vType vc)) := match t with | tleaf _ _ => [] | vleaf vcc var => match (DeqVarSym vcc vc) with | left eqq => [transport eqq var] | right _ => [] end | tnode _ mix => mAllVars mix end with pAllVars {G : CFGV} { vc : VarSym G} {gs : (GSym G)} (p : Pattern gs) {struct p} : (list (vType vc)) := match p with | ptleaf _ _ => [] | pvleaf vcc var => match (DeqVarSym vcc vc) with | left eqq => [transport eqq var] | right _ => [] end | pnode _ mix => mAllVars mix | embed _ t => tAllVars t end with mAllVars {G : CFGV} { vc : VarSym G} {lgs : list (bool * GSym G)} (pts : Mixture lgs) {struct pts} : (list (vType vc)) := match pts with | mnil => [] | mtcons _ _ ph ptl => (tAllVars ph) ++ (mAllVars ptl) | mpcons _ _ ph ptl => (pAllVars ph) ++ (mAllVars ptl) end.
imports: CFGV Omega