K example, equivalence with the (N), (D) rule set
Definition k_n_rule(r : sequent_rule KV KL) : Prop :=
assumptions r = [[lf_prop 0]] ∧ conclusion r = [box_v 0].
Definition k_d_rule(r : sequent_rule KV KL) : Prop :=
∃(sa : sequent KV KL),
assumptions r = [sa] ∧ list_reorder sa (k_assumption 2) ∧
list_reorder (conclusion r) (k_conclusion 2).
Definition k_nd_rules : set (sequent_rule KV KL) :=
union k_n_rule k_d_rule.
Lemma rule_multiset_k_nd : rule_multiset k_nd_rules.
Lemma provable_k_nd_hyp_list_reorder :
∀(hyp : set (sequent KV KL))(s1 s2 : sequent KV KL),
sequent_multiset hyp →
list_reorder s1 s2 →
provable k_nd_rules hyp s1 →
provable k_nd_rules hyp s2.
Lemma k_nd_subset : subset k_nd_rules k_rules.
Lemma k_n_rule_eq_1 : ∀(r : sequent_rule KV KL),
k_n_rule r →
r = k_rule 0.
End K_nd.