proposition: Theorem inTripletsIn : forall (t : triplet) (L : list triplet) (v : rZ), inTriplet v t -> In t L -> inTriplets v L.
proof: Proof. intros t L; elim L; simpl in |- *; auto with stalmarck. intros v H' H'0; elim H'0; auto with stalmarck. intros a l H' v H'0 H'1; elim H'1; intros H'2; auto with stalmarck; rewrite H'2; auto with stalmarck. Qed.