fact: Fixpoint normal (r:regexp) : Prop := match r with | regexp_null => True | regexp_empty => True | regexp_char c => True | regexp_alt r1 r2 => normal r1 /\ normal r2 | regexp_seq r1 r2 => normal r1 /\ normal r2 | regexp_star r1 => productive r1 /\ normal r1 end.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat