proposition: Lemma blocked : forall c : Config, (co c <= 0)%Z -> ~ (exists t : transition c, True).
proof: Proof. intros. unfold not in |- *; intro. elim H0. intro. elim x. intro. intuition. intro. intuition. Qed.
imports: ZArith Omega