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