Formulae are either interpreted over Prop or bool.
A cnf tracking annotations of atoms.
Type parameters
Our cnf is optimised and detects contradictions on the fly.
TX is Prop in Coq and EConstr.constr in Ocaml.
AF is unit in Coq and Names.Id.t in Ocaml
Records annotations used to optimise the cnf.
Those need to be kept when pruning the formula.
For efficiency, this is a separate function.