proposition: Theorem doTripletEq : forall (S1 S2 S3 : State) (t : triplet), doTripletP S1 t S2 -> doTripletP S1 t S3 -> eqState S2 S3.
proof: Proof. intros S1 S2 S3 t H' H'0. red in |- *; split; apply doTripletBisIncl with (S1 := S1) (t := t); auto with stalmarck. Qed.