FALSE_CONSEQ_CONV
ConseqConv.FALSE_CONSEQ_CONV : conseq_conv
Given a term t
of type bool
this
consequence conversion returns the theorem
|- F ==> t
.
ConseqConv.TRUE_CONSEQ_CONV
,
ConseqConv.REFL_CONSEQ_CONV
,
ConseqConv.TRUE_FALSE_REFL_CONSEQ_CONV