proposition: Lemma varTripletTriplet1 : forall (p q r : rZ) (b : rBoolOp) (L : list triplet), In (Triplet b p q r) L -> In p (varTriplets L).
proof: Proof. simple induction L; simpl in |- *; auto with stalmarck. intros t L' HR Ht; elim Ht; intros Ht1; [ rewrite Ht1 | case t ]; simpl in |- *; auto with stalmarck. Qed.