proposition: Lemma inTripletsVarTriplet : forall (L : list triplet) (a : rZ), inTriplets a L -> In a (varTriplets L) \/ In (rZComp a) (varTriplets L).
proof: Proof. intros L; elim L; simpl in |- *; auto with stalmarck. intros a H'; case (eqRzElim _ _ H'); intros H'1; rewrite H'1; auto with stalmarck. intros a; case a; auto with stalmarck. intros r r0 r1 r2 l H' a0 H'0; Elimc H'0; intros H'0; auto with stalmarck. simpl in H'0; Casec H'0; intros H'0; [ idtac | Casec H'0; intros H'0 ]; case (eqRzElim _ _ H'0); intros H'1; rewrite H'1; simpl in |- *; auto with stalmarck. elim (H' _ H'0); auto with datatypes stalmarck. Qed.