proposition: Lemma flatmap_ind {A B: UU} (P: ∏ (x: maybe A), UU): (P nothing) → (∏ a: A, P (just a)) → ∏ x: maybe A, P x.
proof: Proof. intros Pnothing Pjust. induction x as [ok | error]. - exact (Pjust ok). - induction error. exact Pnothing. Defined.
imports: UniMath.Foundations.PartC