proposition: Theorem doTripletEqComp : forall (t : triplet) (S1 S2 S3 S4 : State), doTripletP S1 t S3 -> doTripletP S2 t S4 -> eqState S1 S2 -> eqState S3 S4.
proof: Proof. intros t S1 S2 S3 S4 H' H'0 H'1. elim (doTripletEqCompEx S1 S3 S2 t); [ intros S5 E; Elimc E; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. apply eqStateTrans with (S2 := S5); auto with stalmarck. apply doTripletEq with (S1 := S2) (t := t); auto with stalmarck. Qed.