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