proposition: Theorem doTripletBisIncl : forall (t : triplet) (S1 S2 : State), doTripletP S1 t S2 -> forall S3 : State, doTripletP S1 t S3 -> inclState S3 S2.
proof: Proof. intros t S1 S2 H12 S3 H13. apply realizeStateInclInv; intros f Pfzero Pf2; unfold realizeState in |- *; intros i j Pij; apply realizeStateInv with (S := S3); auto with stalmarck. cut (realizeState f S1); [ intros Pf1 | idtac ]. apply realizeStateEval with (S1 := S1) (t := t); auto with stalmarck. apply evalRealizeState with (S1 := S1) (S2 := S2); auto with stalmarck. apply realizeStateIncl with (S1 := S2); auto with stalmarck. apply doTripletIncl with (t := t); auto with stalmarck. Qed.