proposition: Theorem doTripletsRestrictInv : forall (S1 S2 : State) (L : list triplet), doTripletsP (restrictState S1 (ResTriplets L)) L S2 -> doTripletsP S1 L (unionState (restrictState S2 (ResTriplets L)) S1).
proof: Proof. intros S1 S2 L H'. lapply (restrictDoTripletsComp S1 S2 L); [ intros H'3 | idtac ]; auto with stalmarck. apply doTripletsComp with (S1 := unionState S1 (restrictState S1 (ResTriplets L))) (S2 := unionState S1 S2); auto with stalmarck. apply doTripletCongruent; auto with stalmarck. red in |- *; split; auto with stalmarck. apply unionStateMin; auto with stalmarck. apply restrictStateIncl; auto with stalmarck. apply eqStateTrans with (S2 := unionState S2 S1); auto with stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)