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