proposition: Theorem unionStatePIncl : forall S1 S2 S3 S4 : State, unionStateP S1 S2 S3 -> inclState S1 S4 -> inclState S2 S4 -> inclState S3 S4.
proof: Proof. intros S1 S2 S3 S4 H' H'0 H'1; inversion H'; auto with stalmarck. Qed.
imports: Coq(List)