proposition: Theorem interStatePIncl : forall S1 S2 S3 S4 : State, interStateP S1 S2 S3 -> inclState S4 S1 -> inclState S4 S2 -> inclState S4 S3.
proof: Proof. intros S1 S2 S3 S4 H H1 H2; case H; intros H' H'1; case H'1; auto with stalmarck. Qed.
imports: Coq(List)