Updated demo, at moment only induct_simp tactic is reliable, due to Isabelle renaming library theorems. Should make FO-tactic roubust to this