[DeriveMode False False, Match 0, Mark [[0, 0, 1]], CreateInvariant True, Mark [[0]], DeriveMode True False, Narrow 3 True, Mark [], Simplify 100 True, Mark [], DeriveMode False False, Mark [[0, 1]], ShiftSubs, Mark [], Induction False, Mark [[0, 0, 0, 0], [0, 1, 0, 0, 0], [0, 1, 1, 1, 0, 0], [0, 2, 0, 0, 0], [0, 2, 1, 1, 0, 0]], Narrow 0 False, Mark [], Simplify 100 True, Mark [[0, 0, 1, 0], [0, 1, 0]], Theorem False (F "=" [F "flatten" [F "++" [V "p", V "p'"]], F "++" [F "flatten" [V "p"], F "flatten" [V "p'"]]]), Mark [[0, 0, 1, 0, 1], [0, 1, 0, 1]], Narrow 0 False, Mark [[0, 0, 1, 0, 1, 1], [0, 1, 0, 1, 1]], Narrow 0 False, Mark [[0, 0, 1, 0, 1, 1, 1]], Narrow 0 False, Mark [], Simplify 100 True, Mark []]