PrintForm Definitions graph 1 1 Sections Graphs Doc

At: list accum append
l1,l2:Top List, f,y:Top. list_accum(x,a.f(x,a);y;l1 @ l2) ~ list_accum(x,a.f(x,a);list_accum(x,a.f(x,a);y;l1);l2)
By:
Analyze 0
THEN
ListInd -1
THEN
Reduce 0
THEN
UnivCD
THEN
Trivial ORELSE EasyHyp
Generated subgoals:

None

About:
listsqequaltopall

PrintForm Definitions graph 1 1 Sections Graphs Doc