proposition: Lemma curry_f_comp : FunctorLaws.comp curry_f.
proof: Proof. by rewrite /FunctorLaws.comp => A B C g h; rewrite /curry_f; apply funext => -[]. Qed.
imports: ssrmatching mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy