# Commit 2022-09-25 08:17 8cd94b84

View on Github →feat(order/symm_diff): Heyting bi-implication (#16544)
Define `bihimp`

, the Heyting bi-implication operator. This is dual to `symm_diff`

and generalizes `iff`

on propositions.
Delete `order.imp`

as all the material there is now fully superseded by the Heyting algebra material (`himp`

, defined in `order.heyting.basic`

).