You don't need a rule system to understand what equality is. Yes, it is not computational for sure. It's a logic, not a programming language. Nil is the way u

You don't need a rule system to understand what equality is. Yes, it is not computational for sure. It's a logic, not a programming language. Nil is the way undefinedness is handled in Practal. It is the most elegant way I can think of. You can still have your option type, just as you can have Kleene logic operators, but these are more suitable for doing program verification work in Practal, not so much for doing general mathematics in Practal. You really want (T ∪ Nil) ∪ Nil = T ∪ Nil here, while in programming you usually don't want Option[Option[T]] to be the same as Option[T]. I am not saying it is easy to make all of this work, and to make it work soundly. But less just doesn't cut it. With a kernel-based approach, you have a chance to get it right. If you find an inconsistency, fix the kernel, and move on. Automation works just on top of it, and doesn't affect soundness. This is the great thing about automation in kernel-based ITP: If it finds some solution or counter-example, great. Otherwise, no harm done.