[Clear, ApplyCoinduction False, Clear, Simplify 12 True, Clear, Narrow 6 True, Clear, Push [0, 0, 0, 0, 0, 0], ReplaceVar [0, 0] (F "&" [F "=" [F "$" [F "map" [F "f0" []], F "iter1" [F "f0" [], F "f0" [V "x0"]]], F "$" [F "map" [F "f1" []], F "iter1" [F "f1" [], V "x1"]]], F "=" [F "iter1" [F "f0" [], F "f0" [F "f0" [V "x0"]]], F "iter1" [F "f1" [], F "f1" [V "x1"]]]]) (F "f0" []) "f1", Clear, Push [0, 0, 0, 0, 1, 1], ReplaceVar [0, 0] (F "&" [F "=" [F "$" [F "map" [F "f0" []], F "iter1" [F "f0" [], F "f0" [V "x0"]]], F "$" [F "map" [F "f0" []], F "iter1" [F "f0" [], V "x1"]]], F "=" [F "iter1" [F "f0" [], F "f0" [F "f0" [V "x0"]]], F "iter1" [F "f0" [], F "f0" [V "x1"]]]]) (F "f0" [V "x0"]) "x1", Clear, Simplify 7 True, Clear]