fact: Fixpoint tfreevars {G}(vc : VarSym G) {gs} (p : Term gs) : list (vType vc) := match p with | tleaf _ _ => [] | vleaf vcc var => match (DeqVarSym vcc vc) with | left eqq => [transport eqq var] | right _ => [] end | tnode p m => mfreevars vc m (allBndngVars vc p m) end with pfreevars {G} (vc : VarSym G) {gs} (p : Pattern gs) : list (vType vc) := match p with | ptleaf _ _ => [] | pvleaf vcc var => [] | pnode p lpt => mfreevars vc lpt [] | embed vcc nt => tfreevars vc nt end with mfreevars {G} (vc: VarSym G) {lgs} (m: Mixture lgs) (llB : list (list (vType vc))) : list (vType vc) := match m with | mnil => [] | mtcons _ _ h tl => (tfreevars vc h -- lhead llB) ++ mfreevars vc tl (tail llB) | mpcons _ _ h tl => (pfreevars vc h -- lhead llB) ++ mfreevars vc tl (tail llB) end.
imports: CFGV Omega