proposition: Theorem interStateEq : forall S1 S2 S3 S4 : State, eqState S1 S3 -> eqState S2 S4 -> eqState (interState S1 S2) (interState S3 S4).
proof: Proof. intros S1 S2 S3 S4 H' H'0; red in |- *; split; apply interMemMin; auto with stalmarck. apply inclStateEqStateComp with (S1 := interState S1 S2) (S3 := S1); auto with stalmarck. apply inclStateEqStateComp with (S1 := interState S1 S2) (S3 := S2); auto with stalmarck. apply inclStateEqStateComp with (S1 := interState S3 S4) (S3 := S3); auto with stalmarck. apply inclStateEqStateComp with (S1 := interState S3 S4) (S3 := S4); auto with stalmarck. Qed.
imports: Coq(List)