proposition: Theorem doTripletRestrict : forall (S1 S2 : State) (t : triplet) (L : list rNat), doTripletP S1 t S2 -> incl (ResTriplet t) L -> exists S3 : State, doTripletP (restrictState S1 L) t S3 /\ eqState (restrictState S2 L) S3.
proof: Proof. intros S1 S2 t L H' H'0; inversion H'; simple apply doTripletRestrictAux1 with (1 := H) || apply doTripletRestrictAux2 with (1 := H); rewrite <- H0 in H'0; simpl in H'0; simpl in |- *; repeat rewrite valRzComp; auto with datatypes stalmarck; apply restrictStateComp; repeat rewrite valRzComp; auto with datatypes stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)