Simplifying the proof of NoRetractToModalProposition.paradox in

Hurkens.v by dropping the artificial need for monad laws. Tactic eauto
decided to be dependent on the laws but there is a shorter proof
without them.

[Interestingly, eauto is not able to find the short proof. This is a
situation of the form

subgoal 1:  H : ?A |- P x
subgoal 2:  H : M ?A |- M (forall x, P x)

where addressing the second subgoal would find the right instance of
?A, but this instance is too hard to find by addressing first the
first subgoal.]

0 files changed, 0 insertions, 0 deletions