Declare Scope valid_scope.
Delimit Scope valid_scope with valid.

Infix "++" := FAnd (right associativity, at level 60) : valid_scope.

Module Type VALID.

Parameter valid : term -> Prop.

Local Notation "a ||- b" := (valid (FImp a b)) (at level 61) : valid_scope.
Local Notation "||- b" := (valid b) (at level 61) : valid_scope.
Local Notation "a ⟛ b" := (valid (FImp a b) /\ valid (FImp b a)) (at level 61) : valid_scope.
Local Open Scope valid_scope.

Axiom valid_assumption : forall f, f ||- f.

Axiom valid_top :
  forall f,
  f ||- FTop.
Axiom valid_top_l1 :
  forall f,
  FTop ||- f ->
       ||- f.
Axiom valid_top_l2 :
  forall f,
       ||- f ->
  FTop ||- f.

Axiom valid_contradiction :
  forall f,
  FBot ||- f.
Axiom valid_consistent :
  ~ ||- FBot.

Axiom valid_and_intro :
  forall f g h,
  f ||- g ->
  f ||- h ->
  f ||- g ++ h.
Axiom valid_and_elim :
  forall f g h,
  f ||- g ++ h ->
  f ||- g /\ f ||- h.
Axiom valid_and_intro_l :
  forall f g h,
  g ||- f \/ h ||- f ->
  g ++ h ||- f.
Axiom valid_and_l_cycle :
  forall f1 f2 f3 g,
  f1 ++ f2 ++ f3 ||- g ->
  f3 ++ f1 ++ f2 ||- g.

Axiom valid_imp_intro :
  forall f g h,
  g ++ f ||- h ->
       f ||- (FImp g h).
Axiom valid_imp_elim :
  forall f g h,
  g ++ f ++ FImp f g ||- h ->
       f ++ FImp f g ||- h.

Axiom valid_weak :
  forall f1 f2 g,
        f2 ||- g ->
  f1 ++ f2 ||- g.
Axiom valid_contr :
  forall f g,
  f ++ f ||- g ->
       f ||- g.
Axiom valid_cut :
  forall f g h,
  f ||- g ->
  g ||- h ->
  f ||- h.

Axiom valid_all_mono :
  forall f g,
  f ||- g ->
  FAll f ||- FAll g.
Axiom valid_all_and :
  forall f g,
  FAll (f ++ g) ⟛ FAll f ++ FAll g.
Axiom valid_all_de_bruijn :
  forall f g,
  f.[ren (+1)] ||- g ->
             f ||- FAll g.
Axiom valid_all_elim :
  forall f t,
  FAll f ||- f.[t/].

End VALID.