proposition: Theorem restrictDoTripletComp : forall (S1 S2 : State) (t : triplet) (L : list rNat), incl (ResTriplet t) L -> doTripletP (restrictState S1 L) t S2 -> eqState S2 (restrictState S2 L).
proof: Proof. intros S1 S2 t L H' H'0; inversion H'0; auto with stalmarck; rewrite <- H0 in H'; simpl in H'; apply restrictDoTripletCompAux1 || apply restrictDoTripletCompAux2; auto with datatypes stalmarck; repeat rewrite valRzComp; auto with datatypes stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)