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