proposition: Corollary parse_fix' : forall r s k, normal r -> parse (r,s,k) = Parse parse (r,s,k).
proof: Proof. Proof using. intros. applys~ parse_fix. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat