proposition: Theorem realizeStateIncl : forall (f : rNat -> bool) (S1 S2 : State), realizeState f S1 -> inclState S2 S1 -> realizeState f S2.
proof: Proof. intros f S1 S2 H' H'0; red in |- *; auto with stalmarck. intros i j H'1. apply realizeStateInv with (S := S1); auto with stalmarck. Qed.
imports: Coq(List)