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