# Axioms

- There are several kinds of axioms that can be generated in the code outputted by
`coq-of-ocaml`

. - For the exceptions (typically
`assert`

) we can avoid them using the right pre-conditions when calling functions so that we do not go into these branches. - For GADTs there are:
`unreachable_gadt_branch`

: can be avoided using pre-conditions, like for the`assert`

or exceptions;`cast`

that can be eliminated using`cast_eval`

(see https://github.com/formal-land/coq-of-ocaml/blob/master/proofs/Basics.v )`cast_exists`

that is more involved with existential variables that can be introduced by GADTs. It is eliminated like for`cast_eval`

.

- A technique for functions with a lot of axioms, especially GADT axioms, is to rewrite them without axioms (for example using dependent types instead of GADTs) and show that the two are equivalent. Then, it is easier to do the proof on the dependently typed version.