proposition: Fact surj_t_compose X Y Z : surj_t X Y -> surj_t Y Z -> surj_t X Z.
proof: Proof. intros (f & Hf) (g & Hg); exists (fun x => g (f x)). intros z. destruct (Hg z) as (y & Hy). destruct (Hf y) as (x & Hx). exists x; subst; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac fin_base fin_choice) Undecidability.Shared.Libs.DLW.Vec(pos vec)