`{!SplEssSurj (G o F)} : SplEssSurj G. Proof. intros c. exists (F (esssurj (G o F) c).1). exact ((esssurj (G o F) c).2). Defined.
Require Import Basics.Overture Basics.Tactics Basics.Iff. Require Import WildCat.Core. Require Import WildCat.NatTrans. Require Import WildCat.Sigma.