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