WF_REL_TAC : term quotation -> tactic
STRUCTURE
SYNOPSIS
Initiate a termination proof.
DESCRIPTION
bossLib.WF_REL_TAC is identical to TotalDefn.WF_REL_TAC.
SEEALSO
HOL  Trindemossen-1