proposition: Theorem realizeStateInclInv : forall S1 S2 : State, (forall f : rNat -> bool, f zero = true -> realizeState f S2 -> realizeState f S1) -> inclState S1 S2.
proof: Proof. intros S1 S2 H; apply inclStateIn; intros i j Pij1. case (eqStateRzDec S2 j i); intros Pij2; auto with stalmarck. elim (RealizableCstr S2 i j); auto with stalmarck; intros f Pf; elim Pf; intros Pf1 Pf2. case (EqboolDec (f zero) true); intros P0. generalize (H f P0 Pf1); unfold realizeState in |- *; intros H1. rewrite (H1 i j) in Pf2; auto with stalmarck. generalize Pf2; case (rZEval f j); simpl in |- *; intros Abs; inversion Abs. generalize (H (fun n : rNat => negb (f n)) P0 (RealizeNegb S2 f Pf1)); unfold realizeState in |- *; intros H1. generalize (H1 i j Pij1) Pf2; case i; case j; simpl in |- *; intros n m Abs1; rewrite Abs1; case (f n); simpl in |- *; intros Abs2; inversion Abs2. Qed.