proposition: Lemma varTripletTrue : forall L : list triplet, In rZTrue (varTriplets L).
proof: Proof. simple induction L; simpl in |- *; auto with stalmarck. intros t L' HR; case t; simpl in |- *; auto with stalmarck. Qed.