[Clear, ApplyCoinduction False, Simplify 12 True, Clear, CombineTrees, Clear, Narrow 6 True, Clear, Push [0, 0, 1, 0], ApplyTheorem False (F "=" [F "$" [F "map" [F "$" [F "loop" [F "f" []], V "n"]], F "$" [F "map" [F "f" []], V "s"]], F "$" [F "map" [F "$" [F "loop" [F "f" []], F "suc" [V "n"]]], V "s"]]), Clear, Push [0, 0, 1, 0, 0, 0, 1], ReplaceVar [0] (F "Any F1 N1 X1" [F "&" [F "=" [F "iter1" [F "F0" [], F "F0" [F "$" [F "$" [F "loop" [F "F0" []], V "N0"], V "X0"]]], F "iter1" [F "F1" [], F "$" [F "$" [F "loop" [F "F1" []], V "N1"], V "X1"]]], F "=" [F "$" [F "map" [F "$" [F "loop" [F "F0" []], F "suc" [V "N0"]]], F "iter2" [F "F0" [], V "X0"]], F "$" [F "map" [F "$" [F "loop" [F "F1" []], V "N1"]], F "iter2" [F "F1" [], V "X1"]]]]]) (F "suc" [V "N0"]) "N1", Clear, Push [0, 0, 1, 0, 1, 0], ReplaceVar [0] (F "Any F1 N1 X1" [F "&" [F "=" [F "iter1" [F "F0" [], F "F0" [F "$" [F "$" [F "loop" [F "F0" []], V "N0"], V "X0"]]], F "iter1" [F "F1" [], F "$" [F "$" [F "loop" [F "F1" []], F "suc" [V "N0"]], V "X1"]]], F "=" [F "$" [F "map" [F "$" [F "loop" [F "F0" []], F "suc" [V "N0"]]], F "iter2" [F "F0" [], V "X0"]], F "$" [F "map" [F "$" [F "loop" [F "F1" []], F "suc" [V "N0"]]], F "iter2" [F "F1" [], V "X1"]]]]]) (F "F0" []) "F1", Clear, Push [0, 0, 1, 0, 1, 1], ReplaceVar [0] (F "Any F1 N1 X1" [F "&" [F "=" [F "iter1" [F "F0" [], F "F0" [F "$" [F "$" [F "loop" [F "F0" []], V "N0"], V "X0"]]], F "iter1" [F "F0" [], F "$" [F "$" [F "loop" [F "F0" []], F "suc" [V "N0"]], V "X1"]]], F "=" [F "$" [F "map" [F "$" [F "loop" [F "F0" []], F "suc" [V "N0"]]], F "iter2" [F "F0" [], V "X0"]], F "$" [F "map" [F "$" [F "loop" [F "F0" []], F "suc" [V "N0"]]], F "iter2" [F "F0" [], V "X1"]]]]]) (V "X0") "X1", Clear, Simplify 5 True, Clear, Narrow 1 True, Clear]