wlog_then : term quotation -> term quotation list -> thm_tactic -> tactic
STRUCTURE
wlogLib
SYNOPSIS
Apply a theorem-tactic using a proposition that can be assumed without loss of generality.
DESCRIPTION
wlogLib.wlog_then
is identical to
bossLib.wlog_then
HOL
Trindemossen-1