`{!IsBoundedMeetSemiLattice B} : IsBoundedMeetSemiLattice (A -> B). Proof. repeat split; try apply _; reduce_fun. * apply associativity. * apply left_identity. * apply right_identity. * apply commutativity. * apply binary_idempotent. Defined.
Require Import