`{!SplEssSurj F} : SplEssSurj (G o F) <-> SplEssSurj G. Proof. split; [ apply @cancelR_isesssurj | intros; apply @isesssurj_compose ]; exact _. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Iff. Require Import WildCat.Core. Require Import WildCat.NatTrans. Require Import WildCat.Sigma.