proposition: Lemma negRealizeTriplets : forall (f : rNat -> bool) (L : list triplet), ~ realizeTriplets f L -> ex (fun t : triplet => In t L /\ tEval f t = false).
proof: Proof. simple induction L. intros Abs; absurd (realizeTriplets f nil); auto with stalmarck. intros t L' HR Abs. cut (tEval f t = tEval f t); auto with stalmarck; pattern (tEval f t) at 2 in |- *; case (tEval f t). intros Ht. case (RealizeTripletsDec f L'); intros HL'. absurd (realizeTriplets f (t :: L')); auto with stalmarck. elim (HR HL'); intros t0 H; elim H; exists t0; simpl in |- *; auto with stalmarck. intros H; exists t; auto with datatypes stalmarck. Qed.
imports: Stalmarck(PolyListAux) Stalmarck(makeTriplet)