proposition: Lemma counter_ex : False.
proof: Proof. destruct (cnf_lt_epsilon0_iff l alpha R2) as [H H0]. specialize (H0 R3). eapply lt_irrefl. eapply lt_trans with alpha. apply R1. auto. Qed.
imports: hydras(Schutte AP CNF) Coq(List)