proposition: Theorem makeTripletsIn : forall e : rExpr, match makeTriplets e with | tRC l s n => l <> nil -> inTriplets s l end.
proof: Proof. unfold makeTriplets in |- *; intros e; elim e; simpl in |- *; auto with stalmarck. intros r H'; case H'; auto with stalmarck. intros r; case (makeTripletsFun nil (rnext (maxVar r)) r); auto with stalmarck. intros l r0 H' H'0 H'1. apply inTripletsComp; auto with stalmarck. intros r r0 H' r1 H'0. case (makeTripletsFun nil (rnext (rmax (maxVar r0) (maxVar r1))) r0). intros l r2 r3. case (makeTripletsFun l r3 r1); simpl in |- *; auto with stalmarck. Qed.