PrintForm Definitions graph 1 1 Sections Graphs Doc

At: append assoc sq
a,b,c:Top List. ((a @ b) @ c) ~ (a @ b @ c)
By:
InductionOnList
THEN
UnivCD
THEN
Reduce 0
THEN
Analyze
THEN
EasyHyp
Generated subgoals:

None

About:
listsqequaltopall

PrintForm Definitions graph 1 1 Sections Graphs Doc