proposition: Theorem rZEvalEvalRZMakeTriplets : forall (f : rNat -> bool) (e : rExpr) (l : list triplet) (n : rNat) (s : rZ), realizeTriplets f l -> makeTriplets e = tRC l s n -> rEval f e = rZEval f s.
proof: Proof. intros f e l n s H' H'0. apply sym_equal; auto with stalmarck. apply rZEvalREvalMakeTriplets with (l := l) (n := n); auto with stalmarck. red in |- *; auto with stalmarck. Qed.