proposition: Theorem doTripletsRestrictBis : forall (S1 S2 : State) (L : list triplet), doTripletsP S1 L S2 -> eqState S1 (restrictState S1 (ResTriplets L)) -> eqState S2 (restrictState S2 (ResTriplets L)).
proof: Proof. intros S1 S2 L H' H'0. apply restrictDoTripletsComp with (S1 := S1); auto with stalmarck. apply doTripletsComp with (S1 := S1) (S2 := S2); auto with stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)