proposition: Lemma make_sumtriad_uninformative_1 : forall P Q R: Prop, {P} + {Q} + {R} -> P \/ Q \/ R.
proof: Proof. intros P Q R H. destruct H as [H1 | H2]. - destruct H1. * left. exact p. * right. left. exact q. - right. right. exact H2. Qed.