proposition: Theorem interStatePEq : forall S1 S2 S'1 S'2 S3 S'3 : State, interStateP S1 S2 S3 -> interStateP S'1 S'2 S'3 -> eqState S1 S'1 -> eqState S2 S'2 -> eqState S3 S'3.
proof: Proof. unfold interStateP in |- *. intros S1 S2 S'1 S'2 S3 S'3 H H1 H2 H3; split. generalize (interStatePIncl S'1 S'2) (inclStateEqStateComp S3 S3 S1 S'1) (inclStateEqStateComp S3 S3 S2 S'2). intuition auto using eqStateRef. generalize (interStatePIncl S1 S2) (inclStateEqStateComp S'3 S'3 S'1 S1) (inclStateEqStateComp S'3 S'3 S'2 S2). intuition auto using eqStateRef,eqStateSym. Qed.
imports: Coq(List)