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 i s 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.