trying ULS simplification ltac...
example 3 completed, P_Refl added

The Proves relation (and/or it’s accompanying theorems… which are
relatively nonexistent at the moment…) needs a little love. I added
reflexivity as an axiom (constructor) because… that’s like the simplest
example of a propositional tautological statement, right? if P then P?

Anyway, there currently doesn’t seem to be a way to reason about an
extended environment on the lhs of the Proves relation (i.e., if P
proves Q, then (P /\ R) proves Q… (obviously w/ environments and added
facts, etc - it’s the same thing).
few proof simplifications