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