REFL : conv
STRUCTURE
SYNOPSIS
Returns theorem expressing reflexivity of equality.
DESCRIPTION
REFL maps any term t to the corresponding theorem |- t = t.
FAILURE
Never fails.
SEEALSO
HOL  Trindemossen-1