[DeriveMode False False, Match 2, Mark [[0, 0]], Narrow 0 False, Mark [], Simplify 100 True, Mark [[0, 0, 0]], Narrow 0 False, Mark [[0, 0, 0, 1]], Narrow 0 False, Mark [[0, 0]], Theorem False (F "<===" [F "~" [F "()" [F "upd" [V "i", V "x", V "f"], V "j"], F "()" [V "f", V "j"]], F ">" [V "i", V "j"]]), Mark [[0, 0]], Theorem False (F ">" [F "suc" [V "i"], V "i"]), Mark [], Simplify 100 True, Mark [], Theorem False (F "===>" [F "True" [], F "Any f i" [F "=" [V "s", F "()" [V "f", V "i"]]]]), Mark [], Simplify 100 True, Mark []]