proposition: Theorem evalRealizeState : forall (f : rNat -> bool) (S1 S2 : State) (t : triplet), doTripletP S1 t S2 -> realizeState f S2 -> f zero = true -> tEval f t = true.
proof: Proof. intros f S1 S2 t H'; elim H'; intros p q r H'1 H2 H'3; apply evalRealizeStateAux1 with (1 := H'1) (3 := H2) || apply evalRealizeStateAux2 with (1 := H'1) (3 := H2); try rewrite rZEvalCompInv; try rewrite rZEvalCompInv; simpl in |- *; case (rZEval f p); simpl in |- *; case (rZEval f q); simpl in |- *; case (rZEval f r); simpl in |- *; auto with stalmarck; try repeat rewrite H'3; auto with stalmarck; intuition. Qed.