Theory Ordered_Resolution_Prover_Extra

theory Ordered_Resolution_Prover_Extra
  imports
    "Ordered_Resolution_Prover.Abstract_Substitution"
begin

section ‹Abstract Substitution Extra›

lemma (in substitution_ops) subst_atm_of_eqI:
  "L ⋅l σ⇩L = K ⋅l σ⇩K ⟹ atm_of L ⋅a σ⇩L = atm_of K ⋅a σ⇩K"
  by (cases L; cases K) (simp_all add: subst_lit_def)

lemma (in substitution_ops) set_mset_subst_cls_conv: "set_mset (C ⋅ σ) = (λL. L ⋅l σ) ` set_mset C"
  by (simp add: subst_cls_def)

end