proposition: Theorem inclStateIn : forall S1 S2 : State, (forall a b : rZ, In (a, b) S1 -> eqStateRz S2 a b) -> inclState S1 S2.
proof: Proof. intros S1 S2 H'; red in |- *. intros i j H'0; generalize H'; elim H'0; auto with stalmarck. intros a b L0 H'1 H'2 H'3; apply eqStateRzSym; auto with stalmarck. intros a b c0 L0 H'1 H'2 H'3 H'4 H'5; apply eqStateRzTrans with (b := b); auto with stalmarck. intros a b c0 L0 H'1 H'2 H'3; apply eqStateRzContr with (a := a); auto with stalmarck. Qed.
imports: Coq(List)