proposition: Theorem doTripletsRestrict : forall (S1 S2 : State) (L : list triplet), doTripletsP S1 L S2 -> doTripletsP (restrictState S1 (ResTriplets L)) L (restrictState S2 (ResTriplets L)).
proof: Proof. intros S1 S2 L H'; Elimc H'; clear L S1 S2; auto with stalmarck. intros S1 S2 L H'; apply doTripletsRef; auto with stalmarck. apply restrictEqComp; auto with stalmarck. intros S1 S2 S3 L t H' H'0 H'1 H'2. apply doTripletsRTrans with (S2 := restrictState S2 (ResTriplets L)); auto with stalmarck. elim (doTripletRestrict S1 S2 t (ResTriplets L)); [ intros S4 E; Elimc E; intros H'10 H'11 | idtac | idtac ]; auto with stalmarck. apply doTripletsRTrans with (S2 := restrictState S2 (ResTriplets L)); auto with stalmarck. apply doTripletsTrans with (S2 := S4) (t := t); auto with stalmarck. apply ResTripletInResTriplets; auto with stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)