Dear José,
If it appears alone, impredicativity (self-reference) shouldn't be a problem.
I have tried to give some reasoning from a philosophical perspective here:
The two characteristics of an antinomy: self-reference and negation
https://lists.cam.ac.uk/pipermail/cl-isabelle-use
Hi all,
I observed a strange behavior of the same tactic in HOL-k10 vs HOL-k12
Consider a proof goal
``?!m. ((m = n) \/ m < n) /\ ((if m < n then f m else a) = x)``
e (CONV_TAC(ONCE_DEPTH_CONV COND_ELIM_CONV));
(* In HOL-k10, the tactic results a desired behavior*)
?!m. ((m = n) \/ m < n) /\