proposition: Lemma idfun_inhom (X : obj) : @inhom X X idfun.
proof: Proof. exists (idfun_separated X); rewrite sepfst_idfun sepsnd_idfun; split; exact: idfun_inhom. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib category HB(structures)