Require Export Derivations.


Inductive Derivable (context : flist) (a : form) : Set :=
    Derivable_Intro :
      ∀ t : proof_term, derives context t a → Derivable context a.

Inductive Derivable2 (context : flist) (a b : form) : Set :=
    Derivable2_Intro :
      Derivable context a → Derivable context b → Derivable2 context a b.