proposition: Lemma makeTripletsFunMax : forall (e : rExpr) (l l' : list triplet) (n n' : rNat) (s' : rZ), makeTripletsFun l n e = tRC l' s' n' -> rlt (maxVar e) n -> rVlt s' n'.
proof: Proof. RecExpr. intro H'3. lapply (H' l l0 n n' r0); [ intros H'8; lapply H'8; [ intros H'9; clear H'8 | clear H'8 ] | idtac ]; auto with stalmarck. rewrite <- H2; auto with stalmarck. red in |- *. auto with stalmarck. Qed.