Logic, basic definitions

Formulas, Sequents, Proofs

This is the key module of the formalization. It defines the types for formulas, sequents and proofs. It also defines various subsets of sequents, a measure function on formulas, the modal rank and the functions for extracting the propositional variables.

Require Export dep_lists reorder.

Record modal_operators : Type := {
  operator : Type;
  arity : operator → nat
}.

Section Formulas.
  Variable V : Type.
  Variable L : modal_operators.


Lambda Formulas, page 5


  Inductive lambda_formula : Type :=
    | lf_prop : V → lambda_formula
    | lf_neg : lambda_formula → lambda_formula
    | lf_and : lambda_formula → lambda_formula → lambda_formula
    | lf_modal : ∀(op : operator L),
        counted_list lambda_formula (arity L op) → lambda_formula.


The recursion and induction schemes from Coq are not useful, because of the use of counted_list. I don't like the usual workaround, namely unrolling counted_list and lambda_formula into two mutually recursive types, because it is less modular and, generally, makes a mess. Therefore I have to define my own recursion and induction schemes.
  Fixpoint lambda_formula_rect(T : lambda_formula → Type)
             (prop_fun : ∀(v : V), T (lf_prop v))
             (neg_fun : ∀(f : lambda_formula), T f → T (lf_neg f))
             (and_fun : ∀(f1 f2 : lambda_formula),
                          T f1 → T f2 → T (lf_and f1 f2))
             (modal_fun : ∀(op : operator L)
                            (args : counted_list lambda_formula (arity L op)),
                  (dep_list lambda_formula T (list_of_counted_list args))
                     → T (lf_modal op args))
             (f : lambda_formula) : T f :=
    let rec_fn : ∀(f : lambda_formula), T f :=
          lambda_formula_rect T prop_fun neg_fun and_fun modal_fun
    in
      match f with
        | lf_prop v ⇒ prop_fun v
        | lf_neg f ⇒ neg_fun f (rec_fn f)
        | lf_and f1 f2 ⇒
            and_fun f1 f2 (rec_fn f1) (rec_fn f2)
        | lf_modal op args ⇒
            modal_fun op args
              ((fix map_args(len : nat)(args : counted_list lambda_formula len)
                     : dep_list lambda_formula T (list_of_counted_list args) :=
                  match args with
                    | counted_nil ⇒ dep_nil
                    | counted_cons n f rargs ⇒
                        dep_cons f (list_of_counted_list rargs)
                          (rec_fn f) (map_args n rargs)
                  end
               ) (arity L op) args)
      end.

Induction over lambda_formula's
  Lemma lambda_formula_ind :
    ∀(P : lambda_formula → Prop),
      (∀(v : V), P (lf_prop v)) →
      (∀(f : lambda_formula), P f → P (lf_neg f)) →
      (∀(f1 f2 : lambda_formula), P f1 → P f2 → P (lf_and f1 f2)) →
      (∀(op : operator L)
             (args : counted_list lambda_formula (arity L op)),
         every_nth P (list_of_counted_list args) → P (lf_modal op args))
      →
        ∀(f : lambda_formula), P f.

Define non-dependent recursion over lambda_formula's. As lambda_formula_rect, this contains a nested, inlined, mutually recursive map over counted_list, because, otherwise, Coq won't accept the definition. This is fixed with the next lemma, which references counted_map.
Instead of a separate definition, one could probably derive this from lambda_formula_rect, but for this one needs to transform a dep_list into a counted_list.
  Fixpoint lambda_formula_rec(A : Type)
             (prop_fun : V → A)
             (neg_fun : A → A)
             (and_fun : A → A → A)
             (modal_fun : ∀(op : operator L),
                             counted_list A (arity L op) → A)
           (f : lambda_formula) : A :=
    let rec_fn : ∀(f : lambda_formula), A :=
          lambda_formula_rec A prop_fun neg_fun and_fun modal_fun
    in
      match f with
        | lf_prop v ⇒ prop_fun v
        | lf_neg f ⇒ neg_fun (rec_fn f)
        | lf_and f1 f2 ⇒
            and_fun (rec_fn f1) (rec_fn f2)
        | lf_modal op args ⇒
            modal_fun op
              ((fix map_args(len : nat)(args : counted_list lambda_formula len)
                          : counted_list A len :=
                  match args with
                    | counted_nil ⇒ counted_nil
                    | counted_cons n f rargs ⇒
                        counted_cons (rec_fn f) (map_args n rargs)
                  end
               ) (arity L op) args)
      end.

  Lemma lambda_formula_rec_char :
    ∀(A : Type)(pf : V → A)(nf : A → A)(af : A → A → A)
          (mf : ∀(op : operator L), counted_list A (arity L op) → A)
          (f : lambda_formula),
      lambda_formula_rec A pf nf af mf f =
        match f with
          | lf_prop v ⇒ pf v
          | lf_neg f ⇒ nf (lambda_formula_rec A pf nf af mf f)
          | lf_and f1 f2 ⇒
            af (lambda_formula_rec A pf nf af mf f1)
               (lambda_formula_rec A pf nf af mf f2)
          | lf_modal op args ⇒
            mf op (counted_map (lambda_formula_rec A pf nf af mf) args)
        end.

Utility functions for formulas

Recognizer predicates: these are boolean decidable recognizers. They can be used in functions such as list_search. For specifications there are some Prop valued recognizers below.

  Definition is_prop (l : lambda_formula) : bool :=
    match l with
      | lf_prop _ ⇒ true
      | _ ⇒ false
    end.

  Definition is_neg (l : lambda_formula) : bool :=
    match l with
      | lf_neg _ ⇒ true
      | _ ⇒ false
    end.

  Definition is_and (l : lambda_formula) : bool :=
    match l with
      | lf_and _ _ ⇒ true
      | _ ⇒ false
    end.

  Definition is_modal (l : lambda_formula) : bool :=
    match l with
      | lf_modal _ _ ⇒ true
      | _ ⇒ false
    end.

Accessor functions. These accessor functions work with the decidable recognizers from above.
  Definition get_prop_var(f : lambda_formula)(is_prop_f : is_prop f = true) : V.

  Definition get_neg_form(f : lambda_formula)(is_neg_f : is_neg f = true)
                                                             : lambda_formula.

  Definition get_and_forms(f : lambda_formula)(is_and_f : is_and f = true)
                                             : lambda_formula × lambda_formula.

  Definition get_modal_args(f : lambda_formula)(is_modal_f : is_modal f = true)
                                         : (operator L) × (list lambda_formula).

standard propositional connectives, page 5
  Definition lambda_or(A B : lambda_formula) : lambda_formula :=
    lf_neg(lf_and (lf_neg A) (lf_neg B)).

  Definition lambda_false(nonempty_v : V) : lambda_formula :=
    lf_and (lf_prop nonempty_v) (lf_neg (lf_prop nonempty_v)).

Inversion lemmas for lf_modal


  Lemma lf_modal_inversion_op :
    ∀(op1 op2 : operator L)
          (args1 : counted_list lambda_formula (arity L op1))
          (args2 : counted_list lambda_formula (arity L op2)),
      lf_modal op1 args1 = lf_modal op2 args2 →
        op1 = op2.

  Lemma lf_modal_inversion_args :
    ∀(op : operator L)
          (args1 args2 : counted_list lambda_formula (arity L op)),
      lf_modal op args1 = lf_modal op args2 →
        args1 = args2.

Sequents, Rules


  Definition sequent : Type := list lambda_formula.

  Definition empty_sequent_set : set sequent := empty_set (sequent).

  Record sequent_rule : Type := {
    assumptions: list sequent;
    conclusion: sequent
  }.

simple propositional sequents


  Definition prop_form(f : lambda_formula) : Prop :=
    match f with
      | lf_prop _ ⇒ True
      | _ ⇒ False
    end.

  Definition prop_form_acc(f : lambda_formula)(prop_f : prop_form f) : V.

  Lemma prop_form_acc_tcc_irr :
    ∀(f : lambda_formula)(prop_f_1 prop_f_2 : prop_form f),
      prop_form_acc f prop_f_1 = prop_form_acc f prop_f_2.

  Definition neg_form(f : lambda_formula) : Prop :=
    match f with
      | lf_neg _ ⇒ True
      | _ ⇒ False
    end.

  Lemma neg_form_is_neg :
    ∀(f : lambda_formula), is_neg f = true ↔ neg_form f.

  Definition neg_form_maybe(F : set lambda_formula)(f : lambda_formula)
                                                                     : Prop :=
    match f with
      | lf_neg f ⇒ F f
      | _ ⇒ F f
    end.

  Definition prop_sequent(s : sequent) : Prop :=
    every_nth (neg_form_maybe prop_form) s.

  Lemma prop_sequent_cons :
    ∀(s : sequent)(f : lambda_formula),
      neg_form_maybe prop_form f →
      prop_sequent s →
        prop_sequent (f :: s).

  Lemma prop_sequent_tail :
    ∀(s : sequent)(f : lambda_formula),
      prop_sequent (f :: s) →
        prop_sequent s.

  Lemma prop_sequent_head :
    ∀(s : sequent)(f : lambda_formula),
      prop_sequent (f :: s) →
        neg_form_maybe prop_form f.

  Lemma prop_sequent_list_reorder :
    ∀(s1 s2 : sequent),
      list_reorder s1 s2 →
      prop_sequent s1 →
        prop_sequent s2.

  Fixpoint neg_and_over(fs : set lambda_formula)(f : lambda_formula) : Prop :=
    match f with
      | lf_neg f ⇒ neg_and_over fs f
      | lf_and f1 f2 ⇒ neg_and_over fs f1 ∧ neg_and_over fs f2
      | _ ⇒ fs f
    end.

Formula measure for different purposes


  Definition formula_measure(f : lambda_formula) : nat :=
    lambda_formula_rec nat
      (fun _ ⇒ 0)
      (fun m ⇒ 1 + m)
      (fun m1 m2 ⇒ 2 + m1 + m2)
      (fun _ cl ⇒ 1 + nat_list_sum (list_of_counted_list cl))
    f.

  Lemma formula_measure_char :
    ∀(f : lambda_formula),
      formula_measure f =
        match f with
          | lf_prop _ ⇒ 0
          | lf_neg f ⇒ 1 + (formula_measure f)
          | lf_and f1 f2 ⇒ 2 + (formula_measure f1) + (formula_measure f2)
          | lf_modal _ args ⇒
              1 + nat_list_sum (map formula_measure
                                    (list_of_counted_list args))
        end.

  Definition sequent_measure(s : sequent) : nat :=
    nat_list_sum (map formula_measure s).

  Lemma sequent_measure_cons :
    ∀(s : sequent)(f : lambda_formula),
      sequent_measure (f :: s) =
        (formula_measure f) + (sequent_measure s).

  Lemma sequent_measure_append :
    ∀(sl sr : sequent),
      sequent_measure (sl ++ sr) =
        sequent_measure sl + sequent_measure sr.

  Lemma sequent_measure_context_lt :
   ∀(os ns: sequent)(n : nat)(n_less : n < length os),
     sequent_measure ns
           < formula_measure (nth os n n_less)
     →
       sequent_measure (firstn n os ++ ns ++ skipn (1 + n) os)
         < sequent_measure os.

  Lemma sequent_measure_simple_context_lt :
   ∀(s : sequent)(n : nat)(n_less : n < length s)(f : lambda_formula),
     formula_measure f
           < formula_measure (nth s n n_less)
     →
       sequent_measure (firstn n s ++ f :: skipn (1 + n) s)
         < sequent_measure s.

Proofs

Proofs, page 9
In the paper they use multi-sets for sequents with transparent reorderings in the written representation of a multiset. For the formalization of proofs I have to ensure that sequents of rules are identical, where proof rules are plugged together.
  • The multiset coq library uses functions A -> nat, therefore one cannot use intentional equality on those multisets
  • In a simple list representation I would have to identify lists up to reorderings.
  • This reordering could be built into the rules, complicating all rules.
  • Assuming a total order on V and L I could implement a total order on the formulas and use ordered lists for sequents only. Then intentional equality would be sequent equality. However, reordering calls would be needed in the rules.
  • I therefore push the whole problem now to the conceptual level: I use simple unordered lists and standard equality on them in proofs. Rules and hypothesis must be order invariant.


  Inductive proof(rules : set sequent_rule)(hypotheses : set sequent)
                                                           : sequent → Type :=
    | assume : ∀(gamma : sequent),
        hypotheses gamma → proof rules hypotheses gamma
    | rule : ∀(r : sequent_rule), rules r →
        dep_list sequent (proof rules hypotheses) (assumptions r) →
          proof rules hypotheses (conclusion r).



Recursion for proofs


  Fixpoint proof_rect(rules : set sequent_rule)
             (hypotheses : set sequent)
             (T : sequent → Type)
             (assume_fn : ∀(gamma : sequent), hypotheses gamma → T gamma)
             (rule_fn :
                 ∀(r : sequent_rule)(in_rules : rules r),
                   (dep_list sequent T (assumptions r)) →
                     T (conclusion r))
             (s : sequent)(p : proof rules hypotheses s)
           : T s :=
    match p with
      | assume g g_hyp ⇒ assume_fn g g_hyp
      | rule r r_rules subproofs ⇒
          rule_fn r r_rules
            ((fix map_subproofs(sl : list sequent)
                     (subproofs : dep_list sequent (proof rules hypotheses) sl)
                            : dep_list sequent T sl :=
               match subproofs with
                 | dep_nil ⇒ dep_nil
                 | dep_cons s sl p tl ⇒
                     dep_cons s sl
                       (proof_rect rules hypotheses T assume_fn rule_fn s p)
                       (map_subproofs sl tl)
               end)
              (assumptions r) subproofs)
    end.

  Lemma proof_rect_rule :
    ∀(rules : set sequent_rule)(hypotheses : set sequent)
          (T : sequent → Type)
          (assume_fn : ∀(g : sequent), hypotheses g → T g)
          (rule_fn : ∀(r : sequent_rule)(in_rules : rules r),
             (dep_list sequent T (assumptions r)) → T (conclusion r))
          (r : sequent_rule)(r_rules : rules r)
          (subproofs : dep_list sequent (proof rules hypotheses)
                         (assumptions r)),
      proof_rect rules hypotheses T assume_fn rule_fn (conclusion r)
          (rule rules hypotheses r r_rules subproofs)
      = rule_fn r r_rules
          (dep_map_dep_dep
             (proof_rect rules hypotheses T assume_fn rule_fn)
             (assumptions r) subproofs).

Proof depth


  Definition proof_depth{rules : sequent_rule → Prop}
                        {hypotheses : sequent → Prop}
                        {s : sequent}
                        (p : proof rules hypotheses s) : nat :=
    proof_rect rules hypotheses (fun _ ⇒ nat)
      (fun _ _ ⇒ 1)
      (fun r _ l ⇒ S (nat_list_max (list_of_dep_list (assumptions r) l)))
      s p.

  Lemma proof_depth_assume :
    ∀(rules : set sequent_rule)(hypotheses : set sequent)
          (s : sequent)(in_hyp : hypotheses s),
      proof_depth (assume rules hypotheses s in_hyp) = 1.

  Lemma proof_depth_rule :
    ∀(rules : set sequent_rule)(hypotheses : set sequent)
          (r : sequent_rule)(r_rules : rules r)
          (subproofs : dep_list sequent (proof rules hypotheses)
                         (assumptions r)),
     proof_depth (rule rules hypotheses r r_rules subproofs) =
       1 + (nat_list_max (dep_map_dep_const
                            (@proof_depth rules hypotheses)
                            (assumptions r)
                            subproofs)).

  Lemma proof_depth_rule_le :
    ∀(rules : set sequent_rule)(hypotheses : set sequent)
          (r : sequent_rule)(r_rules : rules r)(n : nat)
          (subproofs : dep_list sequent (proof rules hypotheses)
                         (assumptions r)),
      every_dep_nth
        (fun(s : sequent)(p : proof rules hypotheses s) ⇒ proof_depth p ≤ n)
        (assumptions r)
        subproofs
      → proof_depth (rule rules hypotheses r r_rules subproofs) ≤ S n.

  Lemma proof_depth_rule_le_inv :
    ∀(rules : set sequent_rule)(hypotheses : set sequent)
          (r : sequent_rule)(r_rules : rules r)(n : nat)
          (subproofs : dep_list sequent (proof rules hypotheses)
                         (assumptions r)),
      proof_depth (rule rules hypotheses r r_rules subproofs) ≤ S n →
        every_dep_nth
          (fun(s : sequent)(p : proof rules hypotheses s) ⇒
              proof_depth p ≤ n)
          (assumptions r)
          subproofs.

  Lemma proof_depth_0 :
    ∀(X : Type)
          (rules : sequent_rule → Prop)(hypotheses : sequent → Prop)
          (s : sequent)(p : proof rules hypotheses s),
      proof_depth p ≤ 0 → X.

  Lemma proof_depth_rule_1 :
    ∀(rules : sequent_rule → Prop)(hypotheses : sequent → Prop)
          (r : sequent_rule)(in_rules : rules r)
          (subproofs :
             dep_list sequent (proof rules hypotheses) (assumptions r)),
      proof_depth (rule rules hypotheses r in_rules subproofs) ≤ 1
        → assumptions r = [].

Induction on proofs


  Lemma proof_ind :
    ∀(rules : sequent_rule → Prop)(hypotheses : sequent → Prop)
          (P : ∀(s : sequent), proof rules hypotheses s → Prop),
      (∀(gamma : sequent)(in_hypotheses : hypotheses gamma),
                  P gamma (assume rules hypotheses gamma in_hypotheses)) →
      (∀(r : sequent_rule)(in_rules : rules r)
             (pl : dep_list sequent (proof rules hypotheses) (assumptions r)),
          every_dep_nth P (assumptions r) pl →
                 P (conclusion r) (rule rules hypotheses r in_rules pl)) →
      ∀(s : sequent)(p : proof rules hypotheses s), P s p.

Another, simpler induction scheme. Often, this simple induction suffices.
  Lemma proof_sequent_ind :
    ∀(rules : sequent_rule → Prop)(hypotheses : sequent → Prop)
          (P : sequent → Prop),
      (∀(gamma : sequent), hypotheses gamma → P gamma) →
      (∀(r : sequent_rule),
                rules r → every_nth P (assumptions r) → P (conclusion r))
        → ∀(s : sequent), proof rules hypotheses s → P s.

Provability


  Definition provable(rules : set sequent_rule)(hypotheses : set sequent)
                     (s : sequent) : Prop :=
    ∃ _ : proof rules hypotheses s, True.

  Lemma provable_with_assumption :
    ∀(rules : set sequent_rule)(hypotheses : set sequent)(s : sequent),
      hypotheses s →
        provable rules hypotheses s.

  Lemma provable_with_rule :
    ∀(rules : set sequent_rule)(hypotheses : set sequent)
          (assum : list sequent)(s : sequent),
      rules {| assumptions := assum; conclusion := s |} →
      every_nth (provable rules hypotheses) assum →
        provable rules hypotheses s.

  Definition provable_at_depth(rules : set sequent_rule)
                              (hypotheses : set sequent)
                              (d : nat)
                              (s : sequent) : Prop :=
    ∃ p : proof rules hypotheses s, proof_depth p ≤ d.

  Lemma provable_at_proof_depth :
    ∀(rules : set sequent_rule)(hypotheses : set sequent)(s : sequent)
          (p : proof rules hypotheses s),
      provable_at_depth rules hypotheses (proof_depth p) s.

  Lemma provable_at_depth_provable :
    ∀(rules : set sequent_rule)(hypotheses : set sequent)
          (n : nat)(s : sequent),
      provable_at_depth rules hypotheses n s →
        provable rules hypotheses s.

  Lemma provable_at_depth_0 :
    ∀(P : Prop)
          (rules : sequent_rule → Prop)(hypotheses : sequent → Prop)
          (s : sequent),
      provable_at_depth rules hypotheses 0 s → P.

  Lemma provable_at_depth_with_rule :
    ∀(rules : set sequent_rule)(hypotheses : set sequent)
          (assum : list sequent)(d : nat)(s : sequent),
      rules {| assumptions := assum; conclusion := s |} →
      every_nth (provable_at_depth rules hypotheses d) assum →
        provable_at_depth rules hypotheses (S d) s.

  Lemma provable_at_depth_destruct :
    ∀(rules : set sequent_rule)(hypotheses : set sequent)
          (d : nat)(s : sequent),
      provable_at_depth rules hypotheses (S d) s →
        hypotheses s ∨
        (provable rules hypotheses s ∧
         ∃(r : sequent_rule), rules r ∧
           s = conclusion r ∧
           every_nth (provable_at_depth rules hypotheses d) (assumptions r)).

Induction on the proof depth, formulated with provability
  Lemma proof_depth_sequent_ind :
    ∀(rules : sequent_rule → Prop)(hypotheses : sequent → Prop)
          (P : nat → sequent → Prop),
      (∀(n : nat),
         (∀(s : sequent),
            provable_at_depth rules hypotheses n s → P n s) →
         ∀(s : sequent),
            provable_at_depth rules hypotheses (S n) s → P (S n) s)
      → ∀(s : sequent)(p : proof rules hypotheses s),
           P (proof_depth p) s.

Interpretation of sequents, page 9

The paper uses \hat for this. There are two functions for the finite disjunction of a sequent. The first works on the empty sequent too, but needs a propositional variable to construct false for it. This cannot be used for the TX semantics, because the result is not a prop_modal_prop formula. The second function avoids this by working only on non-empty sequents.
  Fixpoint or_formula_of_sequent_iter(res : lambda_formula)
                                  (l : sequent) : lambda_formula :=
    match l with
      | [] ⇒ res
      | f :: r ⇒ or_formula_of_sequent_iter (lambda_or res f) r
    end.

  Lemma or_formula_of_sequent_iter_append :
    ∀(s1 s2 : sequent)(f : lambda_formula),
      or_formula_of_sequent_iter f (s1 ++ s2) =
        or_formula_of_sequent_iter (or_formula_of_sequent_iter f s1) s2.

  Lemma or_formula_of_sequent_iter_rev :
    ∀(f g : lambda_formula)(s : sequent),
      or_formula_of_sequent_iter f (rev (g :: s)) =
        lambda_or (or_formula_of_sequent_iter f (rev s)) g.

  Definition or_formula_of_sequent(l : sequent)(nonempty_v : V)
                                                           : lambda_formula :=
    match l with
      | [] ⇒ lambda_false nonempty_v
      | f :: r ⇒ or_formula_of_sequent_iter f r
    end.

  Definition or_formula_of_ne_sequent(l : sequent)(nonempty_l : l ≠ [])
                                                           : lambda_formula :=
    match l return l ≠ [] → lambda_formula with
      | [] ⇒ fun(H : [] ≠ []) ⇒ False_rect lambda_formula (H (eq_refl []))
      | f :: r ⇒ fun _ ⇒ or_formula_of_sequent_iter f r
    end nonempty_l.

  Lemma or_formula_of_ne_sequent_tcc_irr :
    ∀(l : sequent)(nonempty_l_1 nonempty_l_2 : l ≠ []),
      or_formula_of_ne_sequent l nonempty_l_1 =
        or_formula_of_ne_sequent l nonempty_l_2.

  Lemma or_formula_of_sequent_nonempty :
    ∀(s : sequent)(nonempty_v : V)(nonempty_s : s ≠ []),
      or_formula_of_sequent s nonempty_v =
        or_formula_of_ne_sequent s nonempty_s.

Proof monotonicity (wrt. the rules and hypothesis)


  Lemma proof_depth_mono :
    ∀(rules1 rules2 : set sequent_rule)(hyp1 hyp2 : set sequent)
          (n : nat)(s : sequent),
      subset rules1 rules2 →
      subset hyp1 hyp2 →
      provable_at_depth rules1 hyp1 n s →
        provable_at_depth rules2 hyp2 n s.

  Lemma proof_mono :
    ∀(rules1 rules2 : set sequent_rule)(hyp1 hyp2 : set sequent)
          (s : sequent),
      subset rules1 rules2 →
      subset hyp1 hyp2 →
      provable rules1 hyp1 s →
        provable rules2 hyp2 s.

  Lemma proof_mono_hyp :
    ∀(rules : set sequent_rule)(hyp1 hyp2 : set sequent)(s : sequent),
      subset hyp1 hyp2 →
      provable rules hyp1 s →
        provable rules hyp2 s.

  Lemma proof_mono_rules :
    ∀(rules1 rules2 : set sequent_rule)(hyp : set sequent)(s : sequent),
      subset rules1 rules2 →
      provable rules1 hyp s →
        provable rules2 hyp s.

  Lemma proof_set_equal :
    ∀(rules1 rules2 : set sequent_rule)(hyp1 hyp2 : set sequent)
          (s : sequent),
      set_equal rules1 rules2 →
      set_equal hyp1 hyp2 →
      provable rules1 hyp1 s →
        provable rules2 hyp2 s.

  Lemma proof_set_equal_rules :
    ∀(rules1 rules2 : set sequent_rule)(hyp : set sequent)
          (s : sequent),
      set_equal rules1 rules2 →
      provable rules1 hyp s →
        provable rules2 hyp s.

Provability is closed under reordering


  Definition sequent_multiset(ss : set sequent) : Prop :=
    ∀(s r : sequent), ss s → list_reorder s r → ss r.

  Lemma sequent_multiset_empty : sequent_multiset empty_sequent_set.

  Definition reordered_rule(or : sequent_rule)(s : sequent)(rr : sequent_rule)
                                                                      : Prop :=
    s = conclusion rr ∧
    length (assumptions or) = length (assumptions rr) ∧
    ∀(n : nat)(n_less_rs : n < length (assumptions or))
          (n_less_rr : n < length (assumptions rr)),
      list_reorder (nth (assumptions or) n n_less_rs)
                   (nth (assumptions rr) n n_less_rr).

  Definition rule_multiset(rs : set sequent_rule) : Prop :=
    ∀(or : sequent_rule)(s : sequent),
      rs or →
      list_reorder (conclusion or) s →
      ∃(rr : sequent_rule),
        reordered_rule or s rr ∧
        rs rr.

  Lemma set_equal_multiset : ∀(rs1 rs2 : set sequent_rule),
    set_equal rs1 rs2 →
    rule_multiset rs1 →
      rule_multiset rs2.

  Lemma multiset_union : ∀(rs1 rs2 : set sequent_rule),
    rule_multiset rs1 →
    rule_multiset rs2 →
      rule_multiset (union rs1 rs2).

  Lemma multiset_depth_provability :
    ∀(rules : set sequent_rule)(hypothesis : set sequent)
          (d : nat)(s r : sequent),
      rule_multiset rules →
      sequent_multiset hypothesis →
      list_reorder s r →
      provable_at_depth rules hypothesis d s →
        provable_at_depth rules hypothesis d r.

  Lemma multiset_provability :
    ∀(rules : set sequent_rule)(hypothesis : set sequent)(s r : sequent),
      rule_multiset rules →
      sequent_multiset hypothesis →
      list_reorder s r →
      provable rules hypothesis s →
        provable rules hypothesis r.

Make sequent multisets out of lists


  Definition reordered_sequent_list_set(l : list sequent) : set sequent :=
    fun(s1 : sequent) ⇒ ∃(s2 : sequent), list_reorder s1 s2 ∧ In s2 l.

  Lemma sequent_multiset_reordered_sequent_list_set :
    ∀(l : list sequent), sequent_multiset (reordered_sequent_list_set l).

Plug proofs for hypothesis


  Lemma plug_hypothesis_proof :
    ∀(rules : set sequent_rule)(provable_hyp hyp : set sequent)
          (s : sequent),
      (∀(h : sequent), provable_hyp h → provable rules hyp h) →
      provable rules (union provable_hyp hyp) s →
        provable rules hyp s.

  Lemma plug_empty_hypothesis_proof :
    ∀(rules : set sequent_rule)(provable_hyp : set sequent)
          (s : sequent),
      (∀(h : sequent), provable_hyp h →
             provable rules empty_sequent_set h) →
      provable rules provable_hyp s →
        provable rules empty_sequent_set s.

Provability with different rules


  Lemma change_rules_hyp_provability :
    ∀(rules1 rules2 : set sequent_rule)(hyp1 hyp2 : set sequent),
      sequent_multiset hyp2 →
      rule_multiset rules2 →
      (∀(r : sequent_rule), rules1 r →
         provable rules2
                  (union (reordered_sequent_list_set (assumptions r)) hyp2)
            (conclusion r)) →
      (∀(h : sequent), hyp1 h → provable rules2 hyp2 h) →
      ∀(s : sequent),
        provable rules1 hyp1 s →
          provable rules2 hyp2 s.

  Lemma change_rules_provability :
    ∀(rules1 rules2 : set sequent_rule),
      rule_multiset rules2 →
      (∀(r : sequent_rule), rules1 r →
         provable rules2 (reordered_sequent_list_set (assumptions r))
             (conclusion r)) →
      ∀(s : sequent),
        provable rules1 empty_sequent_set s →
          provable rules2 empty_sequent_set s.

Modal rank, page 5

In the paper propositional formulas have rank 0, but the paper uses rank -1 in exceptional cases, eg F_n on page 6 and in Lemma 3.7, page 13. There, F{-1} is the empty set.
I therefore use rank 1 for propositional formulas. No formula has rank 0, but the empty sequent has rank 0. Every formula with a modality has at least rank 2, even if the modality has arity 0.
  Definition modal_rank : lambda_formula → nat :=
    lambda_formula_rec nat (fun _ ⇒ 1) id max
      (fun _ (subranks : counted_list nat _) ⇒
         1 + (nat_list_max (1 :: (list_of_counted_list subranks)))).

  Lemma modal_rank_char :
    ∀(f : lambda_formula),
      modal_rank f =
        match f with
          | lf_prop _ ⇒ 1
          | lf_neg f ⇒ modal_rank f
          | lf_and f1 f2 ⇒ max (modal_rank f1) (modal_rank f2)
          | lf_modal op args ⇒
            1 + (nat_list_max
                    (1 :: (map modal_rank (list_of_counted_list args))))
        end.

  Definition minimal_sequent_rank(s : sequent) : nat :=
    nat_list_max (map modal_rank s).


  Lemma modal_rank_ge_1 : ∀(f : lambda_formula),
    0 < modal_rank f.

  Lemma minimal_sequent_rank_gt_0 : ∀(s : sequent),
    s ≠ [] → 0 < minimal_sequent_rank s.

This is used for F_n(\Lambda), page 6
  Definition rank_formula(n : nat) : set lambda_formula :=
    fun(f : lambda_formula) ⇒ modal_rank f ≤ n.

  Lemma rank_formula_zero :
    set_equal (rank_formula 0) (empty_set lambda_formula).

  Lemma rank_formula_zero_TCC :
    ∀(A : Type)(f : lambda_formula), rank_formula 0 f → A.

  Lemma rank_formula_ge :
    ∀(f : lambda_formula)(n1 n2 : nat),
      n1 ≤ n2 →
      rank_formula n1 f →
        rank_formula n2 f.

  Lemma rank_formula_lf_prop : ∀(v : V)(n : nat),
    1 ≤ n → rank_formula n (lf_prop v).

  Lemma rank_formula_lf_neg : ∀(n : nat)(f : lambda_formula),
    rank_formula n (lf_neg f) ↔ rank_formula n f.

  Lemma rank_formula_lf_neg_TCC : ∀(n : nat)(f : lambda_formula),
    rank_formula n (lf_neg f) → rank_formula n f.

  Lemma rank_formula_lf_and : ∀(n : nat)(f1 f2 : lambda_formula),
    rank_formula n f1 → rank_formula n f2 → rank_formula n (lf_and f1 f2).

  Lemma rank_formula_and_left : ∀(n : nat)(f1 f2 : lambda_formula),
    rank_formula n (lf_and f1 f2) → rank_formula n f1.

  Lemma rank_formula_and_right : ∀(n : nat)(f1 f2 : lambda_formula),
    rank_formula n (lf_and f1 f2) → rank_formula n f2.

  Lemma rank_formula_false : ∀(nonempty_v : V)(n : nat),
    1 ≤ n → rank_formula n (lambda_false nonempty_v).

  Lemma rank_formula_neg_form_maybe :
    ∀(fs : set lambda_formula)(n : nat)(f : lambda_formula),
      (∀(f : lambda_formula), fs f → rank_formula n f) →
      neg_form_maybe fs f →
        rank_formula n f.

  Lemma rank_formula_neg_and_over :
    ∀(fs : set lambda_formula)(n : nat)(f : lambda_formula),
      (∀(f : lambda_formula), fs f → rank_formula n f) →
      neg_and_over fs f →
        rank_formula n f.

Unusual argument order because this is used to instantiate form_prop_or in some_neg_form.v.
  Lemma rank_formula_lambda_or :
    ∀(n : nat)(f1 f2 : lambda_formula),
      rank_formula n f1 →
      rank_formula n f2 →
        rank_formula n (lambda_or f1 f2).

  Lemma rank_formula_lambda_or_rev :
    ∀(f1 f2 : lambda_formula)(n : nat),
      rank_formula n (lambda_or f1 f2) →
      rank_formula n f1 ∧ rank_formula n f2.

  Lemma rank_formula_prop_form : ∀(f : lambda_formula),
    prop_form f → rank_formula 1 f.

  Lemma rank_formula_modal :
    ∀(op : operator L)
          (args : counted_list lambda_formula (arity L op))
          (n : nat),
      1 < n →
      every_nth (rank_formula (pred n)) (list_of_counted_list args) →
        rank_formula n (lf_modal op args).

Rank of sequents


  Definition rank_sequent(n : nat) : set sequent :=
    fun(s : sequent) ⇒ every_nth (rank_formula n) s.

  Lemma rank_sequent_mono : ∀(n1 n2 : nat),
    n1 ≤ n2 → subset (rank_sequent n1) (rank_sequent n2).

  Lemma rank_sequent_list_reorder :
    ∀(s1 s2 : sequent)(n : nat), list_reorder s1 s2 →
      ((rank_sequent n s1) ↔ (rank_sequent n s2)).

  Lemma rank_sequent_empty : ∀(n : nat), rank_sequent n [].

  Lemma rank_sequent_cons : ∀(n : nat)(f : lambda_formula)(s : sequent),
    rank_formula n f → rank_sequent n s → rank_sequent n (f :: s).

  Lemma rank_sequent_head : ∀(n : nat)(f : lambda_formula)(s : sequent),
    rank_sequent n (f :: s) → rank_formula n f.

  Lemma rank_sequent_tail : ∀(n : nat)(f : lambda_formula)(s : sequent),
    rank_sequent n (f :: s) → rank_sequent n s.

  Lemma rank_sequent_append :
    ∀(s1 s2 : sequent)(n : nat),
      rank_sequent n s1 → rank_sequent n s2 → rank_sequent n (s1 ++ s2).

  Lemma rank_sequent_append_left :
    ∀(s1 s2 : sequent)(n : nat),
      rank_sequent n (s1 ++ s2) → rank_sequent n s1.

  Lemma rank_sequent_append_right :
    ∀(s1 s2 : sequent)(n : nat),
      rank_sequent n (s1 ++ s2) → rank_sequent n s2.

  Lemma rank_sequent_different_head :
    ∀(n : nat)(f : lambda_formula)(s1 s2 : sequent),
      rank_sequent n (f :: s2) →
      (rank_formula n f → rank_sequent n s1) →
        rank_sequent n (s1 ++ s2).

  Lemma rank_formula_or_formula_iter :
    ∀(s : sequent)(f : lambda_formula)(n : nat),
      rank_sequent n s →
      rank_formula n f →
        rank_formula n (or_formula_of_sequent_iter f s).

  Lemma rank_formula_or_formula_iter_rev :
    ∀(s : sequent)(f : lambda_formula)(n : nat),
      rank_formula n (or_formula_of_sequent_iter f s) →
        rank_formula n f ∧ rank_sequent n s.

  Lemma rank_formula_or_formula_of_sequent :
    ∀(s : sequent)(n : nat)(nonempty_v : V),
      1 ≤ n →
      rank_sequent n s →
        rank_formula n (or_formula_of_sequent s nonempty_v).

The unusual argument order simplifies the proof of state_seq_step_semantics_correct
  Lemma rank_formula_succ_or_formula_of_sequent :
    ∀(n : nat)(nonempty_v : V)(s : sequent),
      rank_sequent (S n) s →
        rank_formula (S n) (or_formula_of_sequent s nonempty_v).

  Lemma rank_formula_or_formula_of_ne_sequent :
    ∀(s : sequent)(n : nat)(nonempty_s : s ≠ []),
      rank_sequent n s →
        rank_formula n (or_formula_of_ne_sequent s nonempty_s).

  Lemma rank_prop_sequent : ∀(s : sequent),
    prop_sequent s → rank_sequent 1 s.

  Lemma rank_sequent_minimal_sequent_rank : ∀(s : sequent),
    rank_sequent (minimal_sequent_rank s) s.

  Lemma rank_sequent_succ_minimal_nonempty_sequent_rank :
    ∀(s : sequent),
      s ≠ [] → rank_sequent (S (pred (minimal_sequent_rank s))) s.

  Lemma rank_sequent_le_minimal : ∀(s : sequent)(n : nat),
    minimal_sequent_rank s ≤ n →
      rank_sequent n s.

  Lemma rank_sequent_ge_minimal : ∀(s : sequent)(n : nat),
    rank_sequent n s → minimal_sequent_rank s ≤ n.

  Lemma rank_formula_modal_ge_2 :
    ∀(op : operator L)
          (args : counted_list lambda_formula (arity L op))
          (n : nat),
      rank_formula n (lf_modal op args) →
        1 < n.

  Lemma rank_formula_modal_1_TCC :
    ∀(A : Type)(op : operator L)
          (args : counted_list lambda_formula (arity L op)),
      rank_formula 1 (lf_modal op args) → A.

  Lemma rank_formula_modal_args_TCC :
    ∀(op : operator L)
          (args : counted_list lambda_formula (arity L op))
          (n : nat),
      rank_formula n (lf_modal op args) →
        every_nth (rank_formula (pred n)) (list_of_counted_list args).

Ranked sequent sets


  Definition rank_sequent_set(n : nat)(ss : set sequent) : Prop :=
    ∀(s : sequent), ss s → rank_sequent n s.

  Lemma rank_sequent_set_empty : ∀(n : nat),
    rank_sequent_set n (empty_sequent_set).

  Lemma rank_sequent_set_mono : ∀(n1 n2 : nat)(ss : set sequent),
    n1 ≤ n2 →
    rank_sequent_set n1 ss →
      rank_sequent_set n2 ss.

  Lemma rank_sequent_set_sequent_list_set :
    ∀(n : nat)(sl : list sequent),
      every_nth (rank_sequent n) sl →
        rank_sequent_set n (reordered_sequent_list_set sl).

Ranked rules

This is used for S_n, page 10
  Definition rule_has_rank(n : nat)(r : sequent_rule) : Prop :=
    every_nth (rank_sequent n) (assumptions r) ∧
    rank_sequent n (conclusion r).

  Definition rank_rules(n : nat)(rules : set sequent_rule) : set sequent_rule :=
    fun(r : sequent_rule) ⇒
      rules r ∧ rule_has_rank n r.

  Lemma subset_rank_rules :
    ∀(n : nat)(rules : set sequent_rule),
      subset (rank_rules n rules) rules.

  Lemma rank_rules_mono :
    ∀(n : nat)(rules1 rules2 : set sequent_rule),
      subset rules1 rules2 →
        subset (rank_rules n rules1) (rank_rules n rules2).

  Lemma rank_rules_set_eq :
    ∀(n : nat)(rules1 rules2 : set sequent_rule),
      set_equal rules1 rules2 →
        set_equal (rank_rules n rules1) (rank_rules n rules2).

  Lemma rank_rules_subset_rank :
    ∀(n1 n2 : nat)(rules : set sequent_rule),
      n1 ≤ n2 →
        subset (rank_rules n1 rules) (rank_rules n2 rules).

  Lemma multiset_rank_rules : ∀(n : nat)(rules : set sequent_rule),
    rule_multiset rules → rule_multiset (rank_rules n rules).

  Lemma provable_rank_rules_hyp_has_rank_n :
    ∀(rules : set sequent_rule)(hyp : set sequent)
          (n : nat)(s : sequent),
      rank_sequent_set n hyp →
      provable (rank_rules n rules) hyp s →
        rank_sequent n s.

  Lemma provable_rank_rules_has_rank_n :
    ∀(rules : set sequent_rule)(n : nat)(s : sequent),
      provable (rank_rules n rules) empty_sequent_set s →
        rank_sequent n s.

  Lemma rank_rules_distribute_union :
    ∀(n : nat)(rules1 rules2 : set sequent_rule),
      set_equal (rank_rules n (union rules1 rules2))
                (union (rank_rules n rules1) (rank_rules n rules2)).

Minimal rank of a rule


  Definition minimal_rule_rank(r : sequent_rule) : nat :=
    nat_list_max ((minimal_sequent_rank (conclusion r)) ::
                  (map minimal_sequent_rank (assumptions r))).

  Lemma minimal_rule_rank_gt_0 : ∀(r : sequent_rule),
    conclusion r ≠ [] →
      0 < minimal_rule_rank r.

  Lemma minimal_rule_rank_assumptions : ∀(r : sequent_rule),
    every_nth (rank_sequent (minimal_rule_rank r)) (assumptions r).

  Lemma minimal_rule_rank_conclusion : ∀(r : sequent_rule),
      rank_sequent (minimal_rule_rank r) (conclusion r).

  Lemma rank_rules_minimal_rule_rank :
    ∀(rules : set (sequent_rule))(r : sequent_rule)(n : nat),
      rules r →
      minimal_rule_rank r ≤ n →
        rank_rules n rules r.

  Lemma rank_rules_ge_minimal : ∀(r : sequent_rule)(n : nat),
    rule_has_rank n r → minimal_rule_rank r ≤ n.

Minimal rank of proofs


  Definition minimal_proof_rank{rules : sequent_rule → Prop}
                               {hypotheses : sequent → Prop}
                               {s : sequent}
                               (p : proof rules hypotheses s) : nat :=
    proof_rect rules hypotheses (fun _ ⇒ nat)
      (fun(s : sequent) _ ⇒ minimal_sequent_rank s)
      (fun(r : sequent_rule) _
          (l : dep_list sequent (fun _ ⇒ nat) (assumptions r)) ⇒
          max (minimal_rule_rank r)
              (nat_list_max (list_of_dep_list (assumptions r) l)))
      s p.

  Lemma minimal_proof_rank_char :
    ∀(rules : set sequent_rule)(hypotheses : set sequent)
          (s : sequent)(p : proof rules hypotheses s),
      minimal_proof_rank p = match p with
        | assume g _ ⇒ minimal_sequent_rank g
        | rule r _ subp ⇒
           max (minimal_rule_rank r)
               (nat_list_max
                   (dep_map_dep_const (@minimal_proof_rank rules hypotheses)
                                      (assumptions r) subp))
      end.

Extract the list of propositional variables


  Definition prop_var_formula : lambda_formula → list V :=
    lambda_formula_rec (list V)
      (fun(v : V) ⇒ [v])
      id
      (@app V)
      (fun(op : operator L)(pl : counted_list (list V) (arity L op)) ⇒
         flatten (list_of_counted_list pl)).

  Definition prop_var_modal_args(n : nat)
                           (args : counted_list lambda_formula n) : list V :=
    flatten ((map prop_var_formula) (list_of_counted_list args)).

  Lemma prop_var_formula_char : ∀(f : lambda_formula),
    prop_var_formula f = match f with
      | lf_prop v ⇒ [v]
      | lf_neg f ⇒ prop_var_formula f
      | lf_and f1 f2 ⇒ (prop_var_formula f1) ++ (prop_var_formula f2)
      | lf_modal op args ⇒ prop_var_modal_args (arity L op) args
    end.

  Lemma prop_var_modal_args_cons :
    ∀(n : nat)(form : lambda_formula)
          (args : counted_list lambda_formula n),
      prop_var_modal_args (S n) (counted_cons form args) =
        (prop_var_formula form) ++ (prop_var_modal_args n args).

  Definition prop_var_sequent(s : sequent) : list V :=
    flatten (map prop_var_formula s).

  Lemma prop_var_sequent_cons :
    ∀(f : lambda_formula)(s : sequent),
      prop_var_sequent (f :: s) = (prop_var_formula f) ++ prop_var_sequent s.

  Lemma prop_var_sequent_append : ∀(s1 s2 : sequent),
    prop_var_sequent (s1 ++ s2) =
      (prop_var_sequent s1) ++ (prop_var_sequent s2).

  Lemma prop_var_sequent_list_reorder : ∀(s1 s2 : sequent),
    list_reorder s1 s2 →
      list_reorder (prop_var_sequent s1) (prop_var_sequent s2).

  Lemma In_prop_var_sequent :
    ∀(v : V)(s : sequent),
      In v (prop_var_sequent s) →
        ∃(f : lambda_formula),
          In v (prop_var_formula f) ∧ In f s.

  Lemma incl_prop_var_formula_sequent :
    ∀(f : lambda_formula)(s : sequent),
      In f s →
        incl (prop_var_formula f) (prop_var_sequent s).

  Lemma prop_var_sequent_cutout_nth : ∀(n : nat)(s : sequent),
    every_nth (fun f ⇒ length (prop_var_formula f) = 1) s →
      prop_var_sequent (cutout_nth s n) = cutout_nth (prop_var_sequent s) n.

End Formulas.

Implicit Arguments lf_prop [[V] [L]].
Implicit Arguments lf_neg [[V] [L]].
Implicit Arguments lf_and [[V] [L]].
Implicit Arguments lf_modal [[V] [L]].
Implicit Arguments lambda_formula_rect [V L].
Implicit Arguments lambda_formula_rec [V L A].
Implicit Arguments is_prop [[V] [L]].
Implicit Arguments is_neg [[V] [L]].
Implicit Arguments is_and [[V] [L]].
Implicit Arguments is_modal [[V] [L]].
Implicit Arguments get_prop_var [V L].
Implicit Arguments get_neg_form [V L].
Implicit Arguments get_and_forms [V L].
Implicit Arguments get_modal_args [V L].
Implicit Arguments lambda_or [V L].
Implicit Arguments lambda_false [V L].
Implicit Arguments lf_modal_inversion_op [V L].
Implicit Arguments assumptions [V L].
Implicit Arguments conclusion [V L].
Implicit Arguments prop_form [[V] [L]].
Implicit Arguments prop_form_acc [V L].
Implicit Arguments neg_form [[V] [L]].
Implicit Arguments neg_form_maybe [V L].
Implicit Arguments prop_sequent [[V] [L]].
Implicit Arguments prop_sequent_head [V L].
Implicit Arguments prop_sequent_tail [V L].
Implicit Arguments neg_and_over [V L].
Implicit Arguments formula_measure [V L].
Implicit Arguments formula_measure_char [V L].
Implicit Arguments sequent_measure [[V] [L]].
Implicit Arguments proof [V L].
Implicit Arguments assume [V L].
Implicit Arguments rule [V L].
Implicit Arguments proof_depth [V L rules hypotheses s].
Implicit Arguments proof_depth_rule [V L].
Implicit Arguments provable [V L].
Implicit Arguments provable_at_depth [V L].
Implicit Arguments proof_depth_sequent_ind [V L].
Implicit Arguments or_formula_of_sequent_iter [V L].
Implicit Arguments or_formula_of_sequent [V L].
Implicit Arguments or_formula_of_ne_sequent [V L].
Implicit Arguments sequent_multiset [V L].
Implicit Arguments reordered_rule [V L].
Implicit Arguments rule_multiset [V L].
Implicit Arguments reordered_sequent_list_set [V L].
Implicit Arguments modal_rank [V L].
Implicit Arguments modal_rank_char [V L].
Implicit Arguments minimal_sequent_rank [V L].
Implicit Arguments modal_rank_ge_1 [V L].
Implicit Arguments rank_formula [V L].
Implicit Arguments rank_formula_ge [V L].
Implicit Arguments rank_formula_lf_neg_TCC [V L].
Implicit Arguments rank_formula_modal_ge_2 [V L].
Implicit Arguments rank_formula_modal_1_TCC [V L].
Implicit Arguments rank_formula_modal_args_TCC [V L].
Implicit Arguments rank_formula_lf_neg [V L].
Implicit Arguments rank_formula_and_left [V L].
Implicit Arguments rank_formula_and_right [V L].
Implicit Arguments rank_formula_lambda_or [V L].
Implicit Arguments rank_sequent [V L].
Implicit Arguments rank_sequent_head [V L].
Implicit Arguments rank_sequent_cons [V L].
Implicit Arguments rank_sequent_list_reorder [V L].
Implicit Arguments rank_sequent_head [V L].
Implicit Arguments rank_sequent_tail [V L].
Implicit Arguments rank_sequent_append [V L].
Implicit Arguments rank_sequent_append_left [V L].
Implicit Arguments rank_sequent_append_right [V L].
Implicit Arguments rank_formula_or_formula_iter_rev [V L].
Implicit Arguments rank_formula_succ_or_formula_of_sequent [V L].
Implicit Arguments rank_sequent_succ_minimal_nonempty_sequent_rank [V L].
Implicit Arguments rank_sequent_set [V L].
Implicit Arguments rule_has_rank [V L].
Implicit Arguments rank_rules [V L].
Implicit Arguments provable_rank_rules_hyp_has_rank_n [V L].
Implicit Arguments rank_rules_distribute_union [V L].
Implicit Arguments minimal_rule_rank [V L].
Implicit Arguments rank_rules_minimal_rule_rank [V L].
Implicit Arguments minimal_proof_rank [V L rules hypotheses s].
Implicit Arguments prop_var_formula [V L].
Implicit Arguments prop_var_formula_char [V L].
Implicit Arguments prop_var_modal_args [V L].
Implicit Arguments prop_var_sequent [[V] [L]].