Require Export classic slice semantics build_proof propositional_models.

Section Step_semantics.

  Variable V : Type.
  Variable L : modal_operators.
  Variable T : functor.

  Fixpoint step_semantics(LS : lambda_structure L T)
                         (f : lambda_formula V L)
                         (n : nat)(rank : rank_formula (S n) f) :
                                         set (terminal_obj_sequence V T n) :=
    match f
      return rank_formula (S n) f → set (terminal_obj_sequence V T n)
    with
      | lf_prop v ⇒
        fun(rank : rank_formula (S n) (lf_prop v)) ⇒
          inv_img (terminal_obj_sequence_pi_2 n) (sets_containing v)
      | lf_neg f ⇒
        fun(rank : rank_formula (S n) (lf_neg f)) ⇒
          set_inverse (step_semantics LS f n
                         (rank_formula_lf_neg_TCC (S n) f rank))
      | lf_and f1 f2 ⇒
        fun(rank : rank_formula (S n) (lf_and f1 f2)) ⇒
          intersection
            (step_semantics LS f1 n (rank_formula_and_left (S n) f1 f2 rank))
            (step_semantics LS f2 n (rank_formula_and_right (S n) f1 f2 rank))
      | lf_modal op args ⇒
        fun(rank : rank_formula (S n) (lf_modal op args)) ⇒
          match n
            return rank_formula (S n) (lf_modal op args) →
                                            set (terminal_obj_sequence V T n)
          with
            | 0 ⇒
              fun(rank : rank_formula 1 (lf_modal op args)) ⇒
                rank_formula_modal_1_TCC _ _ _ rank
            | S n ⇒
              fun(rank : rank_formula (2 + n) (lf_modal op args)) ⇒
                inv_img
                  (terminal_obj_sequence_pi_1 n)
                  (modal_semantics LS op
                     ((fix map_args(len : nat)
                               (args : counted_list (lambda_formula V L) len)
                               (rank : every_nth (rank_formula (S n))
                                                 (list_of_counted_list args))
                           : counted_list
                                   (set (terminal_obj_sequence V T n)) len :=
                       match args
                         in counted_list _ len
                         return every_nth (rank_formula (S n))
                                          (list_of_counted_list args)
                             → counted_list
                                  (set (terminal_obj_sequence V T n)) len
                       with
                         | counted_nil ⇒ fun _ ⇒ counted_nil
                         | counted_cons len f rargs ⇒
                           fun(rank : every_nth (rank_formula (S n))
                                      (f :: (list_of_counted_list rargs))) ⇒
                             counted_cons
                               (step_semantics LS f n
                                                   (every_nth_head _ _ _ rank))
                               (map_args len rargs (every_nth_tail _ _ _ rank))
                       end rank
                      ) (arity L op) args
                        (rank_formula_modal_args_TCC _ _ _ rank)
                     ))
          end rank
    end rank.

  Fixpoint step_semantics_args(LS : lambda_structure L T)(len : nat)
                              (args : counted_list (lambda_formula V L) len)
                              (n : nat)
                              (rank : every_nth (rank_formula (S n))
                                                (list_of_counted_list args))
                     : counted_list (set (terminal_obj_sequence V T n)) len :=
    match args in counted_list _ len
      return every_nth (rank_formula (S n)) (list_of_counted_list args) →
                          counted_list (set (terminal_obj_sequence V T n)) len
    with
      | counted_nil ⇒ fun _ ⇒ counted_nil
      | counted_cons len f rargs ⇒
        fun(rank : every_nth (rank_formula (S n))
                             (f :: (list_of_counted_list rargs))) ⇒
          counted_cons
            (step_semantics LS f n (every_nth_head _ _ _ rank))
            (step_semantics_args LS len rargs n (every_nth_tail _ _ _ rank))
    end rank.

  Lemma step_semantics_modal :
    ∀(LS : lambda_structure L T)
          (op : operator L)
          (args : counted_list (lambda_formula V L) (arity L op))
          (n : nat)(rank : rank_formula (2 + n) (lf_modal op args)),
      step_semantics LS (lf_modal op args) (S n) rank =
      inv_img (terminal_obj_sequence_pi_1 n)
        (modal_semantics LS op
           (step_semantics_args LS (arity L op) args n
              (rank_formula_modal_args_TCC _ _ _ rank))).

  Lemma step_semantics_tcc_irr_eq :
    ∀(LS : lambda_structure L T)(f : lambda_formula V L)
          (n : nat)(rank1 rank2 : rank_formula (S n) f),
      step_semantics LS f n rank1 = step_semantics LS f n rank2.

  Lemma step_semantics_tcc_irr :
    ∀(LS : lambda_structure L T)(n : nat)
          (x : terminal_obj_sequence V T n)(f : lambda_formula V L)
          (rank1 rank2 : rank_formula (S n) f),
      step_semantics LS f n rank1 x → step_semantics LS f n rank2 x.

  Lemma nth_step_semantics_args :
    ∀(LS : lambda_structure L T)
          (len : nat)(args : counted_list (lambda_formula V L) len)
          (n : nat)
          (rank : every_nth (rank_formula (S n)) (list_of_counted_list args))
          (i : nat)(i_less : i < len),
      nth (list_of_counted_list (step_semantics_args LS len args n rank))
        i (less_length_counted_list _ _ _ i_less) =
      step_semantics LS
        (nth (list_of_counted_list args)
             i (less_length_counted_list _ _ _ i_less))
        n (rank i (less_length_counted_list _ _ _ i_less)).

  Lemma step_semantics_lf_neg_rev :
    ∀(LS : lambda_structure L T)(f : lambda_formula V L)(n : nat)
          (rank : rank_formula (S n) f)(x : terminal_obj_sequence V T n),
      not (step_semantics LS f n rank x) →
        step_semantics LS (lf_neg f) n
             (iff_right (rank_formula_lf_neg _ _) rank) x.

  Lemma step_semantics_false :
    ∀(nonempty_v : V)(LS : lambda_structure L T)(n : nat)
          (rank : rank_formula (S n) (lambda_false nonempty_v))
          (x : terminal_obj_sequence V T n),
      not (step_semantics LS (lambda_false nonempty_v) n rank x).

  Definition step_semantics_sequent
             (nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
             (n : nat)(rank : rank_sequent (S n) s) :
                                         set (terminal_obj_sequence V T n) :=
    step_semantics LS (or_formula_of_sequent s nonempty_v) n
                (rank_formula_succ_or_formula_of_sequent n nonempty_v s rank).

  Lemma step_semantics_sequent_tcc_irr :
    ∀(nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
          (n : nat)(rank1 rank2 : rank_sequent (S n) s),
      step_semantics_sequent nonempty_v LS s n rank1 =
      step_semantics_sequent nonempty_v LS s n rank2.

  Lemma step_semantics_sequent_empty :
    ∀(nonempty_v : V)(LS : lambda_structure L T)
          (n : nat)(rank : rank_sequent (S n) []),
      set_equal (step_semantics_sequent nonempty_v LS [] n rank)
                 (empty_set (terminal_obj_sequence V T n)).

  Definition step_semantics_valid
             (nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
             (n : nat)(rank : rank_sequent (S n) s) : Prop :=
    is_full_set (step_semantics_sequent nonempty_v LS s n rank).

  Lemma step_semantics_valid_tcc_irr :
    ∀(nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
          (n : nat)(rank1 rank2 : rank_sequent (S n) s),
      step_semantics_valid nonempty_v LS s n rank1 →
        step_semantics_valid nonempty_v LS s n rank2.

  Lemma step_semantics_valid_nonempty :
    ∀(nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
          (n : nat)(rank : rank_sequent (S n) s),
      step_semantics_valid nonempty_v LS s n rank →
      (∃(x : terminal_obj_sequence V T n), True) →
        s ≠ [].

  Lemma step_semantics_valid_taut :
    ∀(nonempty_v : V)(LS : lambda_structure L T)
          (sigma : lambda_subst V L)(s : sequent V L)
          (k : nat)(rank : rank_sequent (S k) s),
      subst_Ax_set sigma s →
        step_semantics_valid nonempty_v LS s k rank.

  Definition step_semantics_valid_at_rank
             (nonempty_v : V)(LS : lambda_structure L T)(n : nat)
                                                        : set (sequent V L) :=
    fun(s : sequent V L) ⇒
      rank # rank_sequent (S n) s
          /#\ step_semantics_valid nonempty_v LS s n rank.

  Definition slice_model(m : model V T)
                                   : (state m) → slice_obj_T T (state m) V :=
    pair (coalg m) (coval m).

  Lemma semantics_step_semantics :
    ∀(LS : lambda_structure L T)(m : model V T)
          (f : lambda_formula V L)(n : nat)(rank : rank_formula (S n) f),
      set_equal
        (form_semantics LS m f)
        (inv_img (terminal_seq_cone (slice_model m) n)
          (step_semantics LS f n rank)).

  Definition nth_unit_model(c : slice_unit_coalg V T)(n : nat) : model V T :=
    {| state := terminal_obj_sequence V T n;
       coalg := terminal_obj_sequence_pi_1 n ∘ unit_coalg_sequence c n;
       coval := terminal_obj_sequence_pi_2 (S n) ∘ unit_coalg_sequence c n
    |}.

  Lemma slice_model_nth_unit :
    ∀(c : slice_unit_coalg V T)(n : nat),
      slice_model (nth_unit_model c n) ≡ unit_coalg_sequence c n.

  Lemma step_semantics_validity :
    ∀(nonempty_v : V)(LS : lambda_structure L T)(n : nat)
          (s : sequent V L)(rank : rank_sequent (S n) s),
      non_trivial_functor T →
        (valid_all_models nonempty_v LS s ↔
         step_semantics_valid nonempty_v LS s n rank).

  Definition state_seq_step_form_pred(LS : lambda_structure L T)(n : nat)
                                     (x : terminal_obj_sequence V T n)
                                     (f : lambda_formula V L)
                                     (rank_f : rank_formula (S n) f) : Prop :=
         step_semantics LS f n rank_f x.

  Definition state_seq_step_semantics(LS : lambda_structure L T)
                         (s : sequent V L)
                         (n : nat)(rank : rank_sequent (S n) s)
                         (x : terminal_obj_sequence V T n) : Prop :=
    some_neg_dep (rank_formula (S n))
                 (state_seq_step_form_pred LS n x) s rank.

  Lemma state_seq_step_semantics_tcc_irr :
    ∀(LS : lambda_structure L T)(s : sequent V L)
          (n : nat)(rank1 rank2 : rank_sequent (S n) s)
          (x : terminal_obj_sequence V T n),
      state_seq_step_semantics LS s n rank1 x →
        state_seq_step_semantics LS s n rank2 x.

  Lemma state_seq_step_semantics_list_reorder :
    ∀(LS : lambda_structure L T)(s1 s2 : sequent V L)
          (n : nat)(rank : rank_sequent (S n) s2)
          (x : terminal_obj_sequence V T n)
          (reorder : list_reorder s1 s2),
      state_seq_step_semantics LS s1 n
            (iff_left (rank_sequent_list_reorder _ _ (S n) reorder) rank) x →
        state_seq_step_semantics LS s2 n rank x.

  Lemma state_seq_step_semantics_list_reorder_rev :
    ∀(LS : lambda_structure L T)(s1 s2 : sequent V L)
          (n : nat)(rank : rank_sequent (S n) s1)
          (x : terminal_obj_sequence V T n)
          (reorder : list_reorder s1 s2),
      state_seq_step_semantics LS s1 n rank x →
        state_seq_step_semantics LS s2 n
          (iff_right (rank_sequent_list_reorder _ _ (S n) reorder) rank) x.

  Lemma state_seq_step_semantics_append :
    ∀(LS : lambda_structure L T)(s1 s2 : sequent V L)
          (n : nat)(rank : rank_sequent (S n) (s1 ++ s2))
          (x : terminal_obj_sequence V T n),
      state_seq_step_semantics LS (s1 ++ s2) n rank x →
        ~(~state_seq_step_semantics LS s1 n
              (rank_sequent_append_left _ _ _ rank) x ∧
          ¬state_seq_step_semantics LS s2 n
              (rank_sequent_append_right _ _ _ rank) x).

  Lemma state_seq_step_semantics_append_right :
    ∀(LS : lambda_structure L T)(s1 s2 : sequent V L)
          (n : nat)(rank_s1 : rank_sequent (S n) s1)
          (rank_app : rank_sequent (S n) (s1 ++ s2))
          (x : terminal_obj_sequence V T n),
      state_seq_step_semantics LS s1 n rank_s1 x →
        state_seq_step_semantics LS (s1 ++ s2) n rank_app x.

  Lemma state_seq_step_semantics_append_left :
    ∀(LS : lambda_structure L T)(s1 s2 : sequent V L)
          (n : nat)(rank_s2 : rank_sequent (S n) s2)
          (rank_app : rank_sequent (S n) (s1 ++ s2))
          (x : terminal_obj_sequence V T n),
      state_seq_step_semantics LS s2 n rank_s2 x →
        state_seq_step_semantics LS (s1 ++ s2) n rank_app x.

  Lemma state_seq_step_semantics_long_neg_intro :
    ∀(LS : lambda_structure L T)(s : sequent V L)
          (n : nat)(rank : rank_sequent (S n) s)
          (x : terminal_obj_sequence V T n),
      length s ≠ 1 →
      ~~state_seq_step_semantics LS s n rank x →
         state_seq_step_semantics LS s n rank x.

  Lemma state_seq_step_form_pred_lambda_or :
    ∀(LS : lambda_structure L T)(n : nat)
          (x : terminal_obj_sequence V T n)(f1 f2 : lambda_formula V L)
          (rf1 : rank_formula (S n) f1)(rf2 : rank_formula (S n) f2),
      state_seq_step_form_pred LS n x (lambda_or f1 f2)
                              (rank_formula_lambda_or (S n) f1 f2 rf1 rf2)
        ↔
      ~(~state_seq_step_form_pred LS n x f1 rf1 ∧
        ¬ state_seq_step_form_pred LS n x f2 rf2).

  Lemma state_seq_step_semantics_correct :
    ∀(nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
          (n : nat)(rank : rank_sequent (S n) s)
          (x : terminal_obj_sequence V T n),
      state_seq_step_semantics LS s n rank x ↔
        step_semantics_sequent nonempty_v LS s n rank x.

  Definition state_seq_step_semantics_valid
                   (LS : lambda_structure L T)(s : sequent V L)
                   (n : nat)(rank : rank_sequent (S n) s) : Prop :=
    ∀(x : terminal_obj_sequence V T n),
      state_seq_step_semantics LS s n rank x.

  Lemma state_seq_step_semantics_valid_correct :
    ∀(nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
          (n : nat)(rank : rank_sequent (S n) s),
      step_semantics_valid nonempty_v LS s n rank ↔
        state_seq_step_semantics_valid LS s n rank.

  Lemma step_semantics_valid_list_reorder :
    ∀(nonempty_v : V)(LS : lambda_structure L T)(s1 s2 : sequent V L)
          (n : nat)(rank_1 : rank_sequent (S n) s1)
          (rank_2 : rank_sequent (S n) s2),
      list_reorder s1 s2 →
      step_semantics_valid nonempty_v LS s1 n rank_1 →
        step_semantics_valid nonempty_v LS s2 n rank_2.

  Lemma step_semantics_valid_at_rank_list_reorder :
    ∀(nonempty_v : V)(LS : lambda_structure L T)(n : nat)
          (s1 s2 : sequent V L),
      list_reorder s1 s2 →
      step_semantics_valid_at_rank nonempty_v LS n s1 →
        step_semantics_valid_at_rank nonempty_v LS n s2.

  Lemma step_semantics_sequent_append :
    ∀(nonempty_v : V)(LS : lambda_structure L T)(n : nat)
          (s1 s2 : sequent V L)(rank : rank_sequent (S n) (s1 ++ s2)),
      subset
        (step_semantics_sequent nonempty_v LS (s1 ++ s2) n rank)
        (set_inverse
          (intersection
            (set_inverse
               (step_semantics_sequent nonempty_v LS s1 n
                  (rank_sequent_append_left _ _ _ rank)))
            (set_inverse
               (step_semantics_sequent nonempty_v LS s2 n
                  (rank_sequent_append_right _ _ _ rank))))).

  Definition upward_step_correct_rule(nonempty_v : V)(r : sequent_rule V L)
                             (n : nat)(rank : rule_has_rank (S n) r) : Prop :=
    ∀(LS : lambda_structure L T)(x : terminal_obj_sequence V T n),
      step_semantics_sequent nonempty_v LS (conclusion r) n (proj2 rank) x →
        ∀(i : nat)(i_less : i < length (assumptions r)),
          step_semantics_sequent nonempty_v LS (nth (assumptions r) i i_less)
            n (proj1 rank i i_less) x.

  Lemma upward_step_correct_context :
    ∀(nonempty_v : V)(r : sequent_rule V L)(sl sr : sequent V L)(n : nat)
          (rank_context : rule_has_rank (S n) (rule_add_context sl sr r)),
      every_nth (fun(a : sequent V L) ⇒ a ≠ []) (assumptions r) →
      upward_step_correct_rule nonempty_v r n
        (rank_rule_add_context_rev sl sr r (S n) rank_context)
      →
        upward_step_correct_rule nonempty_v (rule_add_context sl sr r)
          n rank_context.


  Lemma upward_step_correct_ax :
    ∀(nonempty_v : V)(r : sequent_rule V L)
          (n : nat)(rank : rule_has_rank (S n) r),
      is_ax_rule r → upward_step_correct_rule nonempty_v r n rank.

  Lemma upward_step_correct_and :
    ∀(nonempty_v : V)(r : sequent_rule V L)
          (n : nat)(rank : rule_has_rank (S n) r),
      is_and_rule r →
        upward_step_correct_rule nonempty_v r n rank.

  Lemma upward_step_correct_neg_and :
    ∀(nonempty_v : V)(r : sequent_rule V L)
          (n : nat)(rank : rule_has_rank (S n) r),
      is_neg_and_rule r →
        upward_step_correct_rule nonempty_v r n rank.

  Lemma upward_step_correct_neg_neg :
    ∀(nonempty_v : V)(r : sequent_rule V L)
          (n : nat)(rank : rule_has_rank (S n) r),
      classical_logic →
      is_neg_neg_rule r →
        upward_step_correct_rule nonempty_v r n rank.

  Lemma upward_step_correct_G :
    ∀(nonempty_v : V)(r : sequent_rule V L)
          (n : nat)(rank : rule_has_rank (S n) r),
      classical_logic →
      G_set V L r →
        upward_step_correct_rule nonempty_v r n rank.

  Lemma step_semantics_valid_G_rule_inductive :
    ∀(nonempty_v : V)(LS : lambda_structure L T)(n : nat),
      classical_logic →
        rule_inductive (G_n_set V L (S n))
                       (step_semantics_valid_at_rank nonempty_v LS n).

  Lemma one_step_semantics_propositional :
    ∀(LS : lambda_structure L T)(n : nat)(f : lambda_formula V L)
          (prop_f : propositional f)(rank : rank_formula (S n) f)
          (x : terminal_obj_sequence V T n),
      step_semantics LS f n rank x ↔
      is_prop_model (terminal_obj_sequence_pi_2 n x) f prop_f.

  Lemma one_step_semantics_valid_propositional :
    ∀(nonempty_v : V)(LS : lambda_structure L T)
          (n : nat)(s : sequent V L)
          (prop_s : propositional_sequent s)(rank : rank_sequent (S n) s),
      non_trivial_functor T →
      step_semantics_valid nonempty_v LS s n rank →
        prop_valid_sequent nonempty_v s prop_s.

  Lemma step_mod_sequent_semantics :
    ∀(nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
          (n : nat)(rank : rank_sequent (2 + n) s),
      prop_modal_sequent s →
        ∃(mod_sem_s : set (obj T (terminal_obj_sequence V T n))),
          set_equal (step_semantics_sequent nonempty_v LS s (S n) rank)
                     (inv_img (terminal_obj_sequence_pi_1 n) mod_sem_s).

  Lemma step_prop_sequent_semantics :
    ∀(nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
          (n : nat)(rank : rank_sequent (S n) s),
      propositional_sequent s →
        ∃(prop_sem_s : set (set V)),
          set_equal (step_semantics_sequent nonempty_v LS s n rank)
                     (inv_img (terminal_obj_sequence_pi_2 n) prop_sem_s).

  Definition n_step_subst_coval(LS : lambda_structure L T)
                    (sigma : lambda_subst V L)
                    (n : nat)(rank_sigma : rank_subst (S n) sigma)
                                  : (terminal_obj_sequence V T n) → set V :=
    fun(x : terminal_obj_sequence V T n)(v : V) ⇒
      step_semantics LS (sigma v) n (rank_sigma v) x.


  Lemma subst_coval_modal_step_semantics :
    ∀(LS : lambda_structure L T)(f : lambda_formula V L)
          (propm_f : prop_modal_prop f)(sigma : lambda_subst V L)(n : nat)
          (rank_subst_f : rank_formula (2 + n) (subst_form sigma f))
          (rank_sigma : rank_subst (S n) sigma)
          (sx : obj T (terminal_obj_sequence V T n))(pv : set V),
      step_semantics LS (subst_form sigma f) (S n) rank_subst_f (sx, pv) ↔
      prop_modal_prop_valuation LS (n_step_subst_coval LS sigma n rank_sigma)
        f propm_f sx.

  Lemma subst_coval_modal_step_semantics_valid :
    ∀(nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
          (nonempty_s : s ≠ [])(propm_s : prop_modal_prop_sequent s)
          (sigma : lambda_subst V L)
          (n : nat)
          (rank_subst_s : rank_sequent (2 + n) (subst_sequent sigma s))
          (rank_sigma : rank_subst (S n) sigma),
      step_semantics_valid nonempty_v LS (subst_sequent sigma s)
        (S n) rank_subst_s
      ↔
      mod_seq_val_valid LS (n_step_subst_coval LS sigma n rank_sigma)
        s nonempty_s propm_s.

  Lemma scssv_4_13_nonempty_tcc :
    ∀(s simple_s : sequent V L)
          (sigma : lambda_subst V L),
      s ≠ [] →
      subst_sequent sigma simple_s = s →
        simple_s ≠ [].

  Lemma subst_coval_modal_step_semantics_valid_for_4_13 :
    ∀(nonempty_v : V)(LS : lambda_structure L T)
          (s simple_s : sequent V L)
          (nonempty_s : s ≠ [])
          (simple_simple_s : simple_modal_sequent simple_s)
          (n : nat)
          (rank : rank_sequent (2 + n) s)
          (sigma : lambda_subst V L)
          (rank_sigma : rank_subst (S n) sigma)
          (s_subst_eq : subst_sequent sigma simple_s = s),
      step_semantics_valid nonempty_v LS s (S n) rank →
      mod_seq_val_valid LS (n_step_subst_coval LS sigma n rank_sigma)
        simple_s (scssv_4_13_nonempty_tcc _ _ _ nonempty_s s_subst_eq)
        (simple_modal_sequent_is_prop_modal_prop _ simple_simple_s).

  Lemma subst_coval_prop_step_semantics :
    ∀(LS : lambda_structure L T)(f : lambda_formula V L)
          (prop_f : propositional f)(sigma : lambda_subst V L)(n : nat)
          (rank_subst_f : rank_formula (S n) (subst_form sigma f))
          (rank_sigma : rank_subst (S n) sigma),
      set_equal
        (step_semantics LS (subst_form sigma f) n rank_subst_f)
        (propositional_valuation (n_step_subst_coval LS sigma n rank_sigma)
           f prop_f).

  Lemma subst_coval_prop_step_semantics_valid :
    ∀(nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
          (prop_s : propositional_sequent s)
          (sigma : lambda_subst V L)
          (n : nat)
          (rank_subst_s : rank_sequent (S n) (subst_sequent sigma s))
          (rank_sigma : rank_subst (S n) sigma),
      prop_seq_val_valid nonempty_v
                (n_step_subst_coval LS sigma n rank_sigma) s prop_s →
        step_semantics_valid nonempty_v LS (subst_sequent sigma s)
          n rank_subst_s.

End Step_semantics.

Implicit Arguments step_semantics_valid [V L T].
Implicit Arguments slice_model [V T].
Implicit Arguments nth_unit_model [V T].
Implicit Arguments step_semantics_valid_nonempty [V L T].
Implicit Arguments step_semantics_valid_at_rank [V L T].
Implicit Arguments step_semantics_valid_G_rule_inductive [V L T].
Implicit Arguments step_mod_sequent_semantics [V L T].
Implicit Arguments step_prop_sequent_semantics [V L T].
Implicit Arguments n_step_subst_coval [V L T].
Implicit Arguments subst_coval_modal_step_semantics_valid_for_4_13 [V L T].