proposition: Lemma ext (B : F -| G) : eta A = eta B -> eps A = eps B -> A = B.
proof: Proof. move: A B => [? ? ? ?] [? ? ? ?] /= ? ?; subst. congr mk; exact/proof_irr. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)