I should've actually looked at SMT-LIB 3.0 way sooner! They're moving to a dependently-typed language! I'm way more excited now!
Wonder if that opens up the door to specify proofs in the same language!
It currently explicitly says there's no type 'prop' of propositions, but adding an explicitly classical prop would make that... very possible 🤩
