proposition: Theorem doTripletConfl : forall (t1 t2 : triplet) (S1 S2 S3 S4 S5 : State), doTripletP S1 t1 S2 -> doTripletP S2 t2 S4 -> doTripletP S1 t2 S3 -> doTripletP S3 t1 S5 -> eqState S4 S5.
proof: Proof. intros t1 t2 S1 S2 S3 S4 S5 H' H'0 H'1 H'2. elim (doTripletConflEx t1 t2 S1 S2 S3); [ intros S6 E; Elimc E; intros S7 E0; Elimc E0; intros H'10 H'11; Elimc H'11; intros H'12 H'13 | idtac | idtac ]; auto with stalmarck. apply eqStateTrans with (S2 := S6). apply doTripletEqComp with (t := t2) (S1 := S2) (S2 := S2); auto with stalmarck. apply eqStateTrans with (S2 := S7); auto with stalmarck. apply doTripletEqComp with (t := t1) (S1 := S3) (S2 := S3); auto with stalmarck. Qed.