proposition: Lemma sumbool_weaken_left: forall P P' Q: Prop, (P -> P') -> ({P} + {Q}) -> ({P'} + {Q}).
proof: Proof. intros. destruct H0; [left | right]; auto. Qed.
imports: Coq.Relations.Relation_Definitions Coq.Lists.List Coq.Program.Basics