proposition: Theorem rZEvalREvalMakeTriplets : forall (f g : rNat -> bool) (e : rExpr) (l : list triplet) (n : rNat) (s : rZ), equalBefore (rnext (maxVar e)) f g -> realizeTriplets g l -> makeTriplets e = tRC l s n -> rZEval g s = rEval f e.
proof: Proof. intros f g e l n s H' H'0 H'1. elim (extendEvalMakeTriplets f e l n s); [ intros g0 E; elim E; intros H'8 H'9; elim H'9; intros H'10 H'11; rewrite H'11; clear H'9 E | idtac ]; auto with stalmarck. apply equalBeforeMakeTriplets with (e := e) (l := l) (n := n); auto with stalmarck. apply (equalBeforeTrans (rnext (maxVar e))) with (y := f); auto with stalmarck. apply (equalBeforeSym (rnext (maxVar e))); auto with stalmarck. Qed.