[Hol-info] Strange tactic behavior HOL-k10 vs HOL-k12

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) /\

[Hol-info] The Principle of Mathematical Induction – Re: [Coq-Club] I don't believe Coinduction; Please help me grok it :)

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