fact: Fixpoint PatInMix {s :GSym G} {l : list (bool # GSym G)} (pt : Pattern s) (mix : Mixture l) : [univ] := match mix with | mnil => False | mpcons s' _ h mtl => {p : s =s' $ transport p pt = h} [+] (PatInMix pt mtl) | mtcons s' _ h mtl => (PatInMix pt mtl) end.
imports: CFGV Omega