proposition: Lemma sepsnd_idfun X : sepsnd (idfun_separated X) = idfun.
proof: Proof. apply funext=> x /=. suff: inr (A:=el X.1) (sepsnd (idfun_separated X) x) = inr x by move=> [=]. by rewrite sepsndK. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib category HB(structures)