Formulas Prop(Lambda(S)) or V

The proof of 5.6 uses a set of formulas whoose members are either propositional variables or modal formulas.

Require Export modal_formulas.

Section Plain_prop_mod.

  Variable V : Type.
  Variable L : modal_operators.

Plain propositional or modal formulas

Used in the proof of 5.6
This is almost the same as prop_or_mod_formula, only that in the latter a single negation is permitted.
  Definition plain_prop_or_mod_formula : set (lambda_formula V L) :=
    union prop_form modal_form.

  Definition plain_prop_mod_subst(subst : lambda_subst V L) : Prop :=
    ∀(v : V), plain_prop_or_mod_formula (subst v).

  Lemma plain_prop_mod_id_subst : plain_prop_mod_subst id_subst.

  Lemma plain_prop_mod_subst_update :
    ∀(v_eq : eq_type V)(sigma : lambda_subst V L)
          (v : V)(f : lambda_formula V L),
      plain_prop_or_mod_formula f →
      plain_prop_mod_subst sigma →
        plain_prop_mod_subst (function_update v_eq sigma v f).

End Plain_prop_mod.

Implicit Arguments plain_prop_or_mod_formula [V L].
Implicit Arguments plain_prop_mod_subst [V L].