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