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