proposition: Lemma sepsndK X Y (f : ele X -> ele Y) (Hf : separated f) (x : el X.2) : inr (sepsnd Hf x) = f (inr x).
proof: Proof. move: X Y f Hf => [X1 X2] [Y1 Y2] /= f [/= Hf1 Hf2] in x *. by case: (cid (Hf2 x)) => y ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib category HB(structures)