proposition: Lemma sepfst_comp X Y Z (f : ele X -> ele Y) (g : ele Y -> ele Z) (Hf : separated f) (Hg : separated g) : sepfst (comp_separated Hf Hg) = sepfst Hg \o sepfst Hf.
proof: Proof. apply funext=> x /=. suff: inl (B := el Z.2) (sepfst (comp_separated Hf Hg) x) = inl (sepfst Hg (sepfst Hf x)) by case. by rewrite 3!sepfstK. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib category HB(structures)