proposition: Theorem unionStateMin : forall S1 S2 S3 : State, inclState S1 S3 -> inclState S2 S3 -> inclState (unionState S1 S2) S3.
proof: Proof. intros S1 S2 S3 H' H'0. destruct (unionStatePunionState S1 S2); auto with stalmarck. Qed.
imports: Coq(List)