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