PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: nil is append
T:Type, l1,l2:T List. nil = (l1 @ l2) l1 = nil & l2 = nil
By:
UnivCD
THEN
AssertBY (nil = (l1 @ l2) (l1 @ l2) = nil) Auto
THEN
RW (SweepDnC (HypC -1)) 0
THEN
RWO Thm* l1,l2:T List. (l1 @ l2) = nil l1 = nil & l2 = nil 0
Generated subgoals:

None

About:
listniluniverseequalandall

PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc