WF_REL_TAC

TotalDefn.WF_REL_TAC : term quotation -> tactic

Initiate a termination proof.

bossLib.WF_REL_TAC is identical to TotalDefn.WF_REL_TAC.

See also

bossLib.WF_REL_TAC