hooo_dual_rev_neq
should require excluded middle for A, B
#627
Labels
hooo_dual_rev_neq
should require excluded middle for A, B
#627
See #620
Since
hooo_dual_eq
is too strong, a new constructive proof is desirable forhooo_dual_rev_neq
.A such proof exists if excluded middle is required for
A, B
.This is required due to
or::from_de_morgan
being used in the proof.I think this proof is acceptable, given that the only reference to
hooo_dual_rev_neq
is intauto_from_para_transitivity
which requires excluded middle.The text was updated successfully, but these errors were encountered: