proposition: Theorem DilemmaContrad : forall (S : State) (L : list triplet) (a b : rZ), validEquation L a b -> eqStateRz S a (rZComp b) -> ex (fun S' : State => stalmarckP S L S' /\ contradictory S').
proof: Proof. intros S L a b V Eq; apply (DilemmaContradAux (length (varTriplets L)) S L a b); auto with stalmarck. rewrite (nthTailProp2 (length (varTriplets L)) (varTriplets L)); auto with stalmarck. intros a' H; inversion H. Qed.
imports: Stalmarck(PolyListAux) Stalmarck(makeTriplet) Coq(Arith)