TRUE_FALSE_REFL_CONSEQ_CONV
ConseqConv.TRUE_FALSE_REFL_CONSEQ_CONV : directed_conseq_conv
Given a term t of type bool this directed consequence conversion
returns the theorem |- F ==> t for CONSEQ_CONV_STRENGTHEN_direction,
the theorem |- t ==> T for CONSEQ_CONV_WEAKEN_direction and
|- t = t for CONSEQ_CONV_UNKNOWN_direction.
See also
ConseqConv.TRUE_CONSEQ_CONV,
ConseqConv.FALSE_CONSEQ_CONV,
ConseqConv.REFL_CONSEQ_CONV