proposition: Theorem extendEvalMakeTriplets : forall (f : rNat -> bool) (e : rExpr) (l : list triplet) (n : rNat) (s : rZ), makeTriplets e = tRC l s n -> exists g : rNat -> bool, equalBefore (rnext (maxVar e)) f g /\ realizeTriplets g l /\ rEval f e = rZEval g s.
proof: Proof. intros f e l n s H'. apply extendEvalMakeTripletsFun with (l := nil (A:=triplet)) (n' := n); simpl in |- *; auto with stalmarck. Qed.