proposition: Lemma uncurry_f_id X : FunctorLaws.id (@uncurry_f X).
proof: Proof. rewrite /FunctorLaws.id => A; rewrite /uncurry_f; apply boolp.funext => ?. by rewrite compidf. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy