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