proposition: Theorem parse_eq_sem : forall r s, normal r -> (parse (r,s,is_nil) = true) = (sem r s).
proof: Proof. Proof using. extens. iff. apply~ parse_to_sem. apply~ sem_to_parse. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat