Description: tbw-ax2 rederived from merco1 . (Contributed by Anthony Hart, 17-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)