fact: Definition meet_morphism d (T : latticeType d) d' (T' : latticeType d') (f : T -> T') : Prop := {morph f : x y / x `&` y}.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)