proposition: Lemma uncurry_f_comp X : FunctorLaws.comp (@uncurry_f X).
proof: Proof. rewrite /FunctorLaws.comp => A B C g h; rewrite /uncurry_f; apply funext => ?. by rewrite compE compA. Qed.
imports: ssrmatching mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy