Universal quantification instead of list Prop when using formula list forms in Coq
This is a bit of a hack, but list Props are a bit useless in Coq as we
can't have recursive calls inside them without violating the
positivity restriction (I think).