proposition: Theorem doTripletConflEx : forall (t1 t2 : triplet) (S1 S2 S3 : State), doTripletP S1 t1 S2 -> doTripletP S1 t2 S3 -> exists S4 : State, (exists S5 : State, doTripletP S2 t2 S4 /\ doTripletP S3 t1 S5 /\ eqState S4 S5).
proof: Proof. intros t1 t2 S1 S2 S3 H' H'0. elim (doTripletUnionEx S1 S2 t1); [ intros S4 E; rewrite E | idtac ]; auto with stalmarck. elim (doTripletUnionEx S1 S3 t2); [ intros S5 E0; rewrite E0 | idtac ]; auto with stalmarck. elim (doTripletCongruentEx S1 S2 S5 t1); [ intros S6 E1; Elimc E1; intros H'6 H'7 | idtac ]; auto with stalmarck. elim (doTripletCongruentEx S1 S3 S4 t2); [ intros S7 E1; Elimc E1; intros H'8 H'9 | idtac ]; auto with stalmarck. exists S7; exists S6; split; [ idtac | split ]; auto with stalmarck. apply eqStateTrans with (S2 := unionState S4 S3); auto with stalmarck. rewrite E0. apply eqStateTrans with (S2 := unionState S5 S2); auto with stalmarck. rewrite E. apply eqStateTrans with (S2 := unionState (unionState S4 S5) S1); auto with stalmarck. apply unionStateAssoc; auto with stalmarck. apply eqStateTrans with (S2 := unionState (unionState S5 S4) S1); auto with stalmarck. apply eqStateSym; auto with stalmarck. apply unionStateAssoc; auto with stalmarck. Qed.