propDenote version 1
proofs using Holds (compute; taut) working so far

Although props are still represented explicitly with a datatype in Coq
(prop), all of the reasoning about whether or not one proposition
proves another has been moved entirely to reasoning about equivalent
Prop’s in Coq.  prop_denote’ (wrapped in Holds for readability)
transforms props to Props, using alpha-renaming to make every Unknown
value unique (so one unknown does not imply another). Now, instead of
asking Proves P Q?, we just convert this into the requirement that (P’
-> Q’) (the Coq proposition) holds, where P’ and Q’ are the Prop
versions of the props P and Q.

Proofs are now completed entirely with compute; tauto. compute unfolds
Holds (and prop_denote’) via computation and transforms the explicit
props into Props. tauto then solves it if it is in fact a tautology in
propositional logic - thus all of the reasoning about different ways to
prove things (at least strictly propositionally) is entirely dependent
on all of the world already invested in the *complete* tactic tauto.
I’ll have to add more reasoning for when specifics like
Restrict/Remove/ConsUpdate are needed etc…