proposition: Lemma maxVarTripletsRlt : forall (e : rExpr) (l l' : list triplet) (n n' : rNat) (s' : rZ), makeTripletsFun l n e = tRC l' s' n' -> rlt (maxVar e) n -> rlt (maxVarTriplets l) n -> rlt (maxVarTriplets l') n'.
proof: Proof. RecExpr; intros H'0 H'1. rewrite <- H2; rewrite <- H0. lapply (H' l l0 n r1 r0); [ intros H'9; lapply H'9; [ intros H'10; lapply H'10; [ clear H'10 H'9 | clear H'10 H'9 ] | clear H'9 ] | idtac ]; auto with stalmarck. simpl in |- *. apply rmaxRlt; auto with stalmarck. apply rmaxRlt; auto with stalmarck. apply rmaxRlt; auto with stalmarck. apply rltTrans with (y := r3); auto with stalmarck. change (rVlt r2 r3) in |- *. eapply makeTripletsFunMax; eauto with stalmarck. eapply rmaxRltLeft; eauto with stalmarck. eauto with stalmarck. apply rltTrans with (y := r5); auto with stalmarck. change (rVlt r4 r5) in |- *. eapply makeTripletsFunMax; eauto with stalmarck. apply rltTransRnext2 with (m := n); eauto with stalmarck. eapply rmaxRltRight; eauto with stalmarck. apply rltTrans with (y := r5); auto with stalmarck. eapply A; eauto with stalmarck. apply rltTransRnext2 with (m := n); auto with stalmarck. eapply rmaxRltRight; eauto with stalmarck. eauto with stalmarck. eapply H'; eauto with stalmarck. eapply rmaxRltLeft; eauto with stalmarck. Qed.