[Clear, ApplyCoinduction False, Clear, Simplify 12 True, Clear, CombineTrees, Clear, Narrow 7 True, Clear, Push [0, 0, 0, 0, 0, 0, 0, 0], ReplaceVar [0] (F "Any F1 N1 S1" [F "&" [F "=" [F "$" [F "map" [F "$" [F "loop" [F "F0" []], F "suc" [V "N0"]]], F "tail" [V "S0"]], F "$" [F "map" [F "$" [F "loop" [F "F1" []], F "suc" [V "N1"]]], V "S1"]], F "=" [F "$" [F "map" [F "$" [F "loop" [F "F0" []], V "N0"]], F "$" [F "map" [F "F0" []], F "tail" [V "S0"]]], F "$" [F "map" [F "$" [F "loop" [F "F1" []], V "N1"]], F "$" [F "map" [F "F1" []], V "S1"]]]]]) (F "F0" []) "F1", Clear, Push [0, 0, 0, 0, 0, 0, 1, 0], ReplaceVar [0] (F "Any F1 N1 S1" [F "&" [F "=" [F "$" [F "map" [F "$" [F "loop" [F "F0" []], F "suc" [V "N0"]]], F "tail" [V "S0"]], F "$" [F "map" [F "$" [F "loop" [F "F0" []], F "suc" [V "N1"]]], V "S1"]], F "=" [F "$" [F "map" [F "$" [F "loop" [F "F0" []], V "N0"]], F "$" [F "map" [F "F0" []], F "tail" [V "S0"]]], F "$" [F "map" [F "$" [F "loop" [F "F0" []], V "N1"]], F "$" [F "map" [F "F0" []], V "S1"]]]]]) (V "N0") "N1", Clear, Push [0, 0, 0, 0, 1], ReplaceVar [0] (F "Any F1 N1 S1" [F "&" [F "=" [F "$" [F "map" [F "$" [F "loop" [F "F0" []], F "suc" [V "N0"]]], F "tail" [V "S0"]], F "$" [F "map" [F "$" [F "loop" [F "F0" []], F "suc" [V "N0"]]], V "S1"]], F "=" [F "$" [F "map" [F "$" [F "loop" [F "F0" []], V "N0"]], F "$" [F "map" [F "F0" []], F "tail" [V "S0"]]], F "$" [F "map" [F "$" [F "loop" [F "F0" []], V "N0"]], F "$" [F "map" [F "F0" []], V "S1"]]]]]) (F "tail" [V "S0"]) "S1", Clear, Simplify 7 True, Clear, Push [0, 1], ApplyTheorem False (F "=" [F "$" [F "$" [F "loop" [F "f" []], V "n"], F "f" [V "x"]], F "f" [F "$" [F "$" [F "loop" [F "f" []], V "n"], V "x"]]]), Clear, Simplify 2 True, Clear]