proposition: Theorem Realizable2 : forall S : State, ~ contradictory S -> exists f : rNat -> bool, realizeState f S /\ f zero = true.
proof: Proof. intros S HS; elim (Realizable S HS); intros f Hf. case (EqboolDec (f zero) true); intros H. exists f; auto with stalmarck. exists (fun n : rNat => negb (f n)); split; auto with bool stalmarck. Qed.