proposition: Lemma makeTripletsFunIncr : forall (e : rExpr) (l l' : list triplet) (n n' : rNat) (s' : rZ), makeTripletsFun l n e = tRC l' s' n' -> rlt n (rnext n').
proof: Proof. RecExpr. lapply (H' l l0 n n' r0); auto with stalmarck. rewrite <- H2; auto with stalmarck. lapply (H' l l0 n r3 r2); [ intros H'9 | auto with stalmarck ]. lapply (A l0 l2 r3 r5 r4); [ intros H'10 | auto with stalmarck ]. apply rltTrans with (y := rnext r3); auto with stalmarck. Qed.