proposition: Theorem contradictoryEq : forall S1 S2 : State, contradictory S1 -> eqState S1 S2 -> contradictory S2.
proof: Proof. intros S1 S2 H' H'0; inversion H'. exists x; auto with stalmarck. apply eqStateEq with (S1 := S1); auto with stalmarck. Qed.
imports: Stalmarck(interState doTriplet)