proposition: Lemma sepfst_idfun X : sepfst (idfun_separated X) = idfun.
proof: Proof. apply funext=> x /=. suff: inl (B:=el X.2) (sepfst (idfun_separated X) x) = inl x by move=> [=]. by rewrite sepfstK. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib category HB(structures)