proposition: Theorem equalBeforeMakeTriplets : forall (f g : rNat -> bool) (e : rExpr) (l : list triplet) (n : rNat) (s : rZ), equalBefore (rnext (maxVar e)) f g -> realizeTriplets f l -> realizeTriplets g l -> makeTriplets e = tRC l s n -> rZEval f s = rZEval g s.
proof: Proof. intros f g e l n s H' H'0 H'1 H'2. apply equalBeforerZEval with (n := n); auto with stalmarck. apply makeTripletsFunMax with (e := e) (l := nil (A:=triplet)) (l' := l) (n := rnext (maxVar e)); auto with stalmarck. apply equalBeforeMakeTripletsFun with (e := e) (l := nil (A:=triplet)) (l' := l) (n := rnext (maxVar e)) (s' := s); auto with stalmarck. Qed.