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