[DeriveMode False False, Match 0, Mark [[0, 0, 0], [0, 1, 0], [0, 2, 0]], CreateIndHyp, Mark [[1, 0], [1, 1]], Match 2, DeriveMode True False, Mark [[0, 1, 1, 0, 0], [0, 1, 1, 0, 1]], Theorem False (F "<===" [F "&" [F "P" [V "x"], F "Q" [V "y", V "z"]], F "&" [F "&" [F "Nat" [V "x"], F "Nat" [V "y"], F "Nat" [V "z"]], F ">>" [F "()" [V "!x", V "!y", V "!z"], F "()" [V "x", V "y", V "z"]]]]), Mark [[1, 1, 1, 1]], ShiftQuants, Mark [[1, 1, 1, 0, 0], [1, 1, 1, 0, 1]], Theorem False (F "<===" [F "&" [F "P" [V "x"], F "Q" [V "y", V "z"]], F "&" [F "&" [F "Nat" [V "x"], F "Nat" [V "y"], F "Nat" [V "z"]], F ">>" [F "()" [V "!x", V "!y", V "!z"], F "()" [V "x", V "y", V "z"]]]]), Mark [[0, 1, 1, 0, 3]], Theorem False (F "<===" [F ">>" [F "()" [V "x", V "y", V "z"], F "()" [V "x'", V "y'", V "z'"]], F "&" [F ">" [V "x", V "x'"], F ">" [V "x", V "y'"]]]), Mark [[1, 1, 1, 1, 0, 2]], Theorem False (F "<===" [F ">>" [F "()" [V "x", V "y", V "z"], F "()" [V "x'", V "y'", V "z'"]], F "&" [F "`gt`" [F "()" [V "y", V "z"], F "()" [V "x'", F "0" []]], F "`gt`" [F "()" [V "y", V "z"], F "()" [V "y'", V "z'"]]]]), Mark [[1, 1, 1, 1, 0, 2], [1, 1, 1, 1, 0, 3]], Narrow 0 False, Mark [[0, 1, 1, 0, 3]], Theorem False (F ">" [F "suc" [V "x"], V "x"]), Mark [[0, 0, 0]], DeriveMode False False, Mark [[0, 0, 0]], DeriveMode True False, Mark [[1, 1, 1, 0, 2]], Theorem False (F ">" [F "suc" [V "x"], V "x"]), Mark [[0, 2]], Narrow 0 False, Mark []]