proposition: Lemma curry_f_id : FunctorLaws.id curry_f.
proof: Proof. by rewrite /FunctorLaws.id => A; rewrite /curry_f; apply boolp.funext => -[]. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy