Library hydras.solutions_exercises.schutte_cnf_counter_example

From hydras Require Import Schutte AP CNF.
From Coq Require Import List.
Open Scope schutte_scope.

Section Cter_example.

  Hypothesis cnf_lt_epsilon0_iff :
    ∀ l alpha,
      is_cnf_of alpha l →
      (alpha < epsilon0 ↔ Forall (fun beta ⇒ beta < alpha) l).

  Let alpha := phi0 (succ epsilon0).
  Let l := succ epsilon0 :: nil.

  Remark R1 : epsilon0 < alpha.

  Remark R2 : is_cnf_of alpha l.

  Remark R3 : Forall (fun beta ⇒ beta < alpha) l.

  Lemma counter_ex : False.

End Cter_example.