proposition: Lemma not_l_sumbool_rec : forall (A B : Prop) (S : Set) (l r : S), ~ A -> forall H : {A} + {B}, sumbool_rec (fun _ : {A} + {B} => S) (fun x : A => l) (fun x : B => r) H = r.
proof: Proof. intros. elim H0. intro. elim H. assumption. intros. reflexivity. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid