Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Require Import choice fintype finfun finset path fingraph bigop.

Require Import edone bcase fset.

Require Import base dags.
Require Import CTL_def tab_def tab_dec modular_hilbert tab_translation demo tab_complete.

Set Implicit Arguments.
Import Prenex Implicits.

Theorem cert_dec_method (s : form) : {(exists (M:model) (w:M), finite M /\ eval s w)} + { prv (Neg s) }.

Corollary decidability s : decidable (exists (M:model) (w:M), eval s w).

Corollary completeness s : (forall (M:model) (w:M), eval s w) -> prv s.

Lemma disjointness s : ~ ((exists (M:model) (w:M), eval (Neg s) w) /\ prv s).

Print Assumptions cert_dec_method.