K example, Absorption properties and syntactic cut elimination, 5.2, 5.4
Lemma prop_var_sequent_support : ∀(s : sequent KV KL),
prop_sequent s →
every_nth neg_form s →
list_support kv_eq (prop_var_sequent s) =
prop_var_sequent (sequent_support kop_eq kv_eq s).
Lemma k_absorbs_contraction : absorbs_contraction kop_eq kv_eq k_rules.
Theorem k_syntactic_cut :
admissible_rule_set (GR_set k_rules) (empty_sequent_set KV KL) is_cut_rule.
Theorem k_syntactic_contraction :
admissible_rule_set (GR_set k_rules) (empty_sequent_set KV KL)
is_contraction_rule.
End K_absorb.