proposition: Theorem unionStatePAssoc2 : forall S1 S2 S3 S'1 S'2 S'3 : State, unionStateP S2 S3 S'1 -> unionStateP S1 S'1 S'2 -> unionStateP S1 S2 S'3 -> unionStateP S'3 S3 S'2.
proof: Proof. intros S1 S2 S3 S'1 S'2 S'3 H' H'0 H'1. apply unionStatePDef; auto with stalmarck. apply unionStatePIncl with (1 := H'1); auto with stalmarck. inversion H'0; auto with stalmarck. apply inclStateTrans with (S2 := S'1); auto with stalmarck. inversion H'; auto with stalmarck. inversion H'0; auto with stalmarck. apply inclStateTrans with (S2 := S'1); auto with stalmarck. inversion H'; auto with stalmarck. inversion H'0; auto with stalmarck. intros S4 H'2 H'3. apply unionStatePIncl with (1 := H'0); auto with stalmarck. apply inclStateTrans with (S2 := S'3); auto with stalmarck. inversion H'1; auto with stalmarck. apply unionStatePIncl with (1 := H'); auto with stalmarck. apply inclStateTrans with (S2 := S'3); auto with stalmarck. inversion H'1; auto with stalmarck. Qed.
imports: Coq(List)