proposition: Fact idfun_is_set_meet_morphism : set_meet_morphism (@idfun T).
proof: Proof. by move=> B; rewrite image_id. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)