Prove atomization minimizes formulas in coq

[doyougnu]

This repository's issues are reserved for feature requests and bug reports.

• I'm submitting a ...

  • bug report
  • feature request
  • support request

• Do you want to request a feature or report a bug?

• What is the current behavior?

• If the current behavior is a bug, please provide the steps to reproduce and if possible a minimal demo of the problem via
  https://plnkr.co or similar (you can use this template as a starting point: http://plnkr.co/edit/tpl:AvJOMERrnz94ekVua0u5).

• What is the expected behavior?

• What is the motivation / use case for changing the behavior?

• Please tell us about your environment:

  • Version: 2.0.0-beta.X
  • OS: [MacOSX | Windows 10 | Windows 7 | Linux (specify distro)]
  • GHC Version:
  • Solver: [ Z3 | Yices | MathSat | Boolector | ABC | Cvc4 ]
  • Solver Version:

• Other information (e.g. detailed explanation, stacktraces, related issues, suggestions how to fix, links for us to have context, eg. stackoverflow, gitter, etc)