proposition: Theorem realizeStateEvalEquiv : forall (f : rNat -> bool) (S1 S2 : State) (t : triplet), doTripletP S1 t S2 -> realizeState f S1 -> f zero = true -> (realizeState f S2 <-> tEval f t = true).
proof: Proof. intros f S1 S2 H' H'0; red in |- *. split; intros H'1. apply evalRealizeState with (1 := H'0); auto with stalmarck. apply realizeStateEval with (2 := H'0); auto with stalmarck. Qed.