Yes. You could also simplify in the assumptions by using fs[]
which should work. Michael From: Haitao Zhang <zhtp...@gmail.com> Date: Wednesday, 13 March 2019 at 12:27 To: hol-info <hol-info@lists.sourceforge.net> Subject: [Hol-info] Proving a negative statement I want to prove ``a <> b`` for some a,b. After stripping I am asked to prove F. I was able to use the assumptions to prove ``F = T``. At this point I thought "asm_simp_tac bool_ss []" should finish the proof but it doesn't. So "pop_assum (fn th => rewrite_tac [th]" actually finished the work for me. Is this to be expected? Thanks, Haitao
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
