Theory First_Order_Superposition_Completeness

theory First_Order_Superposition_Completeness
  imports
    Ground_Superposition_Completeness
    Grounded_First_Order_Superposition
    "HOL-ex.Sketch_and_Explore"
begin

lemma welltypedσ_on_term:
  assumes "welltypedσ_on (term.vars term) ℱ 𝒱 γ"
  shows "welltyped ℱ 𝒱 term τ ⟷ welltyped ℱ 𝒱 (term ⋅t γ) τ"
  by (simp add: assms welltypedσ_on_welltyped)

context grounded_first_order_superposition_calculus
begin


lemma eq_resolution_lifting:
  fixes 
    premiseG conclusionG :: "'f gatom clause" and 
    premise "conclusion" :: "('f, 'v) atom clause" and
    γ :: "('f, 'v) subst"
  defines 
    premiseG [simp]: "premiseG ≡ clause.to_ground (premise ⋅ γ)" and
    conclusionG [simp]: "conclusionG ≡ clause.to_ground (conclusion ⋅ γ)"
  assumes 
    premise_grounding: "clause.is_ground (premise ⋅ γ)" and
    conclusion_grounding: "clause.is_ground (conclusion ⋅ γ)" and
    select: "clause.from_ground (selectG premiseG) = (select premise) ⋅ γ" and
    ground_eq_resolution: "ground.ground_eq_resolution premiseG conclusionG" and
    typing: 
    "welltypedc typeof_fun 𝒱 premise"
    "term_subst.is_ground_subst γ"
    "welltypedσ_on (clause.vars premise) typeof_fun 𝒱 γ"
    "all_types 𝒱"
  obtains conclusion' 
  where
    "eq_resolution (premise, 𝒱) (conclusion', 𝒱)"
    "Infer [premiseG] conclusionG ∈ inference_groundings (Infer [(premise, 𝒱)] (conclusion', 𝒱))"
    "conclusion' ⋅ γ = conclusion ⋅ γ"
  using ground_eq_resolution
proof(cases premiseG conclusionG rule: ground.ground_eq_resolution.cases)
  case (ground_eq_resolutionI literalG premiseG' termG)

  have premise_not_empty: "premise ≠ {#}"
    using 
      ground_eq_resolutionI(1)
      empty_not_add_mset
      clause_subst_empty
    unfolding premiseG
    by (metis clause_from_ground_empty_mset clause.from_ground_inverse)

  have "premise ⋅ γ = clause.from_ground (add_mset literalG (clause.to_ground (conclusion ⋅ γ)))"
    using 
      ground_eq_resolutionI(1)[THEN arg_cong, of clause.from_ground]
      clause.to_ground_inverse[OF premise_grounding]
      ground_eq_resolutionI(4)
    unfolding premiseG conclusionG
    by metis

  also have "... = add_mset (literal.from_ground literalG) (conclusion ⋅ γ)"
    unfolding clause_from_ground_add_mset
    by (simp add: conclusion_grounding)

  finally have premise_γ: "premise ⋅ γ = add_mset (literal.from_ground literalG) (conclusion ⋅ γ)".

  let ?selectG_empty = "selectG premiseG = {#}"
  let ?selectG_not_empty = "selectG premiseG ≠ {#}"

  obtain max_literal where max_literal: 
    "is_maximall max_literal premise" 
    "is_maximall (max_literal ⋅l γ) (premise ⋅ γ)"
    using is_maximall_ground_subst_stability[OF premise_not_empty premise_grounding]
    by blast

  moreover then have "max_literal ∈# premise"
    using maximall_in_clause by fastforce

  moreover have max_literal_γ: "max_literal ⋅l γ = literal.from_ground (termG !≈ termG)"
    if ?selectG_empty
  proof-
    have "ground.is_maximal_lit literalG premiseG"
      using ground_eq_resolutionI(3) that maximal_lit_in_clause
      by (metis empty_iff set_mset_empty)

    then show ?thesis
      using max_literal(2) unique_maximal_in_ground_clause[OF premise_grounding] 
      unfolding 
        ground_eq_resolutionI(2) 
        is_maximal_lit_iff_is_maximall 
        premiseG 
        clause.to_ground_inverse[OF premise_grounding]
      by blast
  qed

  moreover obtain selected_literal where 
    "selected_literal ⋅l γ = literal.from_ground (termG !≈ termG)" and
    "is_maximall selected_literal (select premise)" 
  if ?selectG_not_empty
  proof-
    have "ground.is_maximal_lit literalG (selectG premiseG)" if ?selectG_not_empty
      using ground_eq_resolutionI(3) that
      by blast

    then show ?thesis 
      using 
        that 
        select 
        unique_maximal_in_ground_clause[OF select_subst(1)[OF premise_grounding]]
        is_maximall_ground_subst_stability[OF _ select_subst(1)[OF premise_grounding]]
      unfolding
        ground_eq_resolutionI(2) 
        premiseG
        is_maximal_lit_iff_is_maximall
      by (metis (full_types) clause_subst_empty(2) clause.from_ground_inverse clause_to_ground_empty_mset)
  qed

  moreover then have "selected_literal ∈# premise" if ?selectG_not_empty
    by (meson that maximall_in_clause mset_subset_eqD select_subset)

  ultimately obtain literal where
    literal_γ: "literal ⋅l γ = literal.from_ground (termG !≈ termG)" and
    literal_in_premise: "literal ∈# premise" and
    literal_selected: "?selectG_not_empty ⟹ is_maximall literal (select premise)" and
    literal_max: "?selectG_empty ⟹ is_maximall literal premise"
    by blast

  have literal_grounding: "literal.is_ground (literal ⋅l γ)"
    using literal_γ
    by simp

  from literal_γ obtain "term" term' where 
    literal: "literal = term !≈ term'"
    using subst_polarity_stable literal_from_ground_polarity_stable
    by (metis literal.collapse(2) literal.disc(2) uprod_exhaust)


  have literalG: 
    "literal.from_ground literalG = (term !≈ term') ⋅l γ" 
    "literalG = literal.to_ground ((term !≈ term') ⋅l γ)"
    using literal_γ literal ground_eq_resolutionI(2) 
    by simp_all

  obtain conclusion' where conclusion': "premise = add_mset literal conclusion'"
    using multi_member_split[OF literal_in_premise]
    by blast

  have "term ⋅t γ = term' ⋅t γ"
    using literal_γ
    unfolding literal subst_literal(2) atom.subst_def literal.from_ground_def atom.from_ground_def
    by simp

  moreover obtain τ where "welltyped typeof_fun 𝒱 term τ" "welltyped typeof_fun 𝒱 term' τ"
    using typing(1) 
    unfolding conclusion' literal welltypedc_def welltypedl_def welltypeda_def
    by auto

  ultimately obtain μ σ where μ: 
    "term_subst.is_imgu μ {{term, term'}}" 
    "γ = μ ⊙ σ" 
    "welltyped_imgu' typeof_fun 𝒱 term term' μ"
    using welltyped_imgu'_exists
    by meson

  have conclusion'_γ: "conclusion' ⋅ γ = conclusion ⋅ γ"
    using premise_γ
    unfolding conclusion' ground_eq_resolutionI(2) literal_γ[symmetric] subst_clause_add_mset
    by simp

  have eq_resolution: "eq_resolution (premise, 𝒱) (conclusion' ⋅ μ, 𝒱)"
  proof (rule eq_resolutionI)
    show "premise = add_mset literal conclusion'"
      using conclusion'.
  next 
    show "literal = term !≈ term'"
      using literal.    
  next
    show "term_subst.is_imgu μ {{term, term'}}"
      using μ(1).
  next
    show "select premise = {#} ∧ is_maximall (literal ⋅l μ) (premise ⋅ μ) 
       ∨  is_maximall (literal ⋅l μ) ((select premise) ⋅ μ)"
    proof(cases ?selectG_empty)
      case selectG_empty: True

      then have "max_literal ⋅l γ = literal ⋅l γ"
        by (simp add: max_literal_γ literal_γ)

      then have literal_γ_is_maximal: "is_maximall (literal ⋅l γ) (premise ⋅ γ)"
        using max_literal(2) by simp

      have literal_μ_in_premise: "literal ⋅l μ ∈# premise ⋅ μ"
        by (simp add: clause.subst_in_to_set_subst literal_in_premise)

      have "is_maximall (literal ⋅l μ) (premise ⋅ μ)"
        using is_maximall_ground_subst_stability'[OF 
            literal_μ_in_premise 
            premise_grounding[unfolded μ(2) clause.subst_comp_subst]
            literal_γ_is_maximal[unfolded μ(2) clause.subst_comp_subst literal.subst_comp_subst]
            ].

      then show ?thesis
        using select selectG_empty
        by clause_auto
    next
      case False

      have selected_grounding: "clause.is_ground (select premise ⋅ μ ⋅ σ)"
        using select_subst(1)[OF premise_grounding]
        unfolding μ(2) clause.subst_comp_subst.

      note selected_subst =
        literal_selected[OF False, THEN maximall_in_clause, THEN clause.subst_in_to_set_subst]

      have "is_maximall (literal ⋅l γ) (select premise ⋅ γ)"
        using False ground_eq_resolutionI(3) 
        unfolding ground_eq_resolutionI(2) is_maximal_lit_iff_is_maximall literal_γ select
        by presburger

      then have "is_maximall (literal ⋅l μ) (select premise ⋅ μ)"
        unfolding μ(2) clause.subst_comp_subst literal.subst_comp_subst
        using is_maximall_ground_subst_stability'[OF selected_subst selected_grounding]
        by argo

      with False show ?thesis
        by blast
    qed
  next 
    show "welltyped_imgu' typeof_fun 𝒱 term term' μ"
      using μ(3).
  next 
    show "conclusion' ⋅ μ = conclusion' ⋅ μ" ..
  qed

  have "term_subst.is_idem μ"
    using μ(1)
    by (simp add: term_subst.is_imgu_iff_is_idem_and_is_mgu)  

  then have μ_γ: "μ ⊙ γ = γ"
    unfolding μ(2) term_subst.is_idem_def
    by (metis subst_compose_assoc)

  have vars_conclusion': "clause.vars (conclusion' ⋅ μ) ⊆ clause.vars premise"
    using vars_clause_imgu[OF μ(1)] 
    unfolding conclusion' literal 
    by clause_auto

  have "conclusion' ⋅ μ ⋅ γ = conclusion ⋅ γ"
    using conclusion'_γ  
    unfolding clause.subst_comp_subst[symmetric] μ_γ.

  moreover have
    "Infer [premiseG] conclusionG ∈ inference_groundings (Infer [(premise, 𝒱)] (conclusion' ⋅ μ, 𝒱))"
    unfolding inference_groundings_def mem_Collect_eq
  proof -
    have "Infer [premiseG] conclusionG ∈ ground.G_Inf"
      unfolding ground.G_Inf_def
      using ground_eq_resolution by blast

    then have "∃ρ1 ρ2. is_inference_grounding
      (Infer [(premise, 𝒱)] (conclusion' ⋅ μ, 𝒱))
      (Infer [premiseG] conclusionG) γ ρ1 ρ2"
      unfolding is_inference_grounding_def Calculus.inference.case list.case prod.case
      using typing
      by (smt (verit) calculation conclusionG eq_resolution eq_resolution_preserves_typing premiseG
          vars_conclusion' welltypedσ_on_subset)

    thus "∃ιG γ ρ1 ρ2. Infer [premiseG] conclusionG = ιG ∧
       is_inference_grounding (Infer [(premise, 𝒱)] (conclusion' ⋅ μ, 𝒱)) ιG γ ρ1 ρ2"
      by iprover
  qed

  ultimately show ?thesis
    using that[OF eq_resolution]
    by blast
qed

lemma eq_factoring_lifting:
  fixes 
    premiseG conclusionG :: "'f gatom clause" and 
    premise "conclusion" :: "('f, 'v) atom clause" and
    γ :: "('f, 'v) subst"
  defines 
    premiseG [simp]: "premiseG ≡ clause.to_ground (premise ⋅ γ)" and
    conclusionG [simp]: "conclusionG ≡ clause.to_ground (conclusion ⋅ γ)"
  assumes
    premise_grounding: "clause.is_ground (premise ⋅ γ)" and
    conclusion_grounding: "clause.is_ground (conclusion ⋅ γ)" and
    select: "clause.from_ground (selectG premiseG) = (select premise) ⋅ γ" and
    ground_eq_factoring: "ground.ground_eq_factoring premiseG conclusionG" and
    typing:
    "welltypedc typeof_fun 𝒱 premise"
    "term_subst.is_ground_subst γ"
    "welltypedσ_on (clause.vars premise) typeof_fun 𝒱 γ"
    "all_types 𝒱"
  obtains conclusion' 
  where
    "eq_factoring (premise, 𝒱) (conclusion', 𝒱)"
    "Infer [premiseG] conclusionG ∈ inference_groundings (Infer [(premise, 𝒱)] (conclusion', 𝒱))"
    "conclusion' ⋅ γ = conclusion ⋅ γ"
  using ground_eq_factoring
proof(cases premiseG conclusionG rule: ground.ground_eq_factoring.cases)
  case (ground_eq_factoringI literalG1 literalG2 premise'G termG1 termG2 termG3)

  have premise_not_empty: "premise ≠ {#}"
    using ground_eq_factoringI(1) empty_not_add_mset clause_subst_empty premiseG
    by (metis clause_from_ground_empty_mset clause.from_ground_inverse)

  have select_empty: "select premise = {#}"
    using ground_eq_factoringI(4) select clause_subst_empty
    by clause_auto

  have premise_γ: "premise ⋅ γ = clause.from_ground (add_mset literalG1 (add_mset literalG2 premise'G))"
    using ground_eq_factoringI(1) premiseG
    by (metis premise_grounding clause.to_ground_inverse)

  obtain literal1 where literal1_maximal: 
    "is_maximall literal1 premise" 
    "is_maximall (literal1 ⋅l γ) (premise ⋅ γ)"
    using is_maximall_ground_subst_stability[OF premise_not_empty premise_grounding]
    by blast

  have max_ground_literal: "is_maximall (literal.from_ground (termG1 ≈ termG2)) (premise ⋅ γ)"
    using ground_eq_factoringI(5)
    unfolding 
      is_maximal_lit_iff_is_maximall 
      ground_eq_factoringI(2) 
      premiseG 
      clause.to_ground_inverse[OF premise_grounding].

  have literal1_γ: "literal1 ⋅l γ = literal.from_ground literalG1"
    using 
      unique_maximal_in_ground_clause[OF premise_grounding literal1_maximal(2) max_ground_literal]
      ground_eq_factoringI(2)
    by blast

  then have "is_pos literal1"
    unfolding ground_eq_factoringI(2)
    using literal_from_ground_stable subst_pos_stable
    by (metis literal.disc(1))

  with literal1_γ obtain term1 term1' where 
    literal1_terms: "literal1 = term1 ≈ term1'" and
    termG1_term1: "term.from_ground termG1 = term1 ⋅t γ"
    unfolding ground_eq_factoringI(2)
    by clause_simp
  
  obtain premise'' where premise'': "premise = add_mset literal1 premise''"
    using maximall_in_clause[OF literal1_maximal(1)]
    by (meson multi_member_split)

  then have premise''_γ: "premise'' ⋅ γ =  add_mset (literal.from_ground literalG2) (clause.from_ground premise'G)"
    using premise_γ 
    unfolding clause_from_ground_add_mset literal1_γ[symmetric]
    by (simp add: subst_clause_add_mset)

  then obtain literal2 where literal2:
    "literal2 ⋅l γ = literal.from_ground literalG2"
    "literal2 ∈# premise''"
    unfolding clause.subst_def
    using msed_map_invR by force

  then have "is_pos literal2"
    unfolding ground_eq_factoringI(3)
    using literal_from_ground_stable subst_pos_stable
    by (metis literal.disc(1))

  with literal2 obtain term2 term2' where 
    literal2_terms: "literal2 = term2 ≈ term2'" and
    termG1_term2: "term.from_ground termG1 = term2 ⋅t γ"
    unfolding ground_eq_factoringI(3) 
    by clause_simp

  have termG2_term1': "term.from_ground termG2 = term1' ⋅t γ"
    using literal1_γ termG1_term1 
    unfolding 
      literal1_terms 
      ground_eq_factoringI(2)       
    apply clause_simp
    by auto

  have termG3_term2': "term.from_ground termG3 = term2' ⋅t γ"
    using literal2 termG1_term2
    unfolding 
      literal2_terms 
      ground_eq_factoringI(3) 
    by clause_auto

  obtain premise' where premise: "premise = add_mset literal1 (add_mset literal2 premise')" 
    using literal2(2) maximall_in_clause[OF  literal1_maximal(1)] premise''
    by (metis multi_member_split)

  then have premise'_γ: "premise' ⋅ γ = clause.from_ground premise'G"
    using premise''_γ  premise''
    unfolding literal2(1)[symmetric]
    by (simp add: subst_clause_add_mset)

  have term1_term2: "term1 ⋅t γ = term2 ⋅t γ"
    using termG1_term1 termG1_term2
    by argo

  moreover obtain τ where "welltyped typeof_fun 𝒱 term1 τ" "welltyped typeof_fun 𝒱 term2 τ"
  proof-
    have "welltypedc typeof_fun 𝒱 (premise ⋅ γ)"
      using typing
      using welltypedσ_on_welltypedc by blast

    then obtain τ where "welltyped typeof_fun 𝒱 (term.from_ground termG1) τ"
      unfolding premise_γ  ground_eq_factoringI 
      by clause_simp

    then have "welltyped typeof_fun 𝒱 (term1 ⋅t γ) τ" "welltyped typeof_fun 𝒱 (term2 ⋅t γ) τ"
      using termG1_term1 termG1_term2
      by metis+

    then have "welltyped typeof_fun 𝒱 term1 τ" "welltyped typeof_fun 𝒱 term2 τ"
      using typing(3) welltypedσ_on_term
      unfolding welltypedσ_on_def premise literal1_terms literal2_terms
      apply clause_simp 
      by (metis UnCI welltypedσ_on_def welltypedσ_on_term)+

    then show ?thesis
      using that
      by blast
  qed

  ultimately obtain μ σ where μ: 
    "term_subst.is_imgu μ {{term1, term2}}" 
    "γ = μ ⊙ σ" 
    "welltyped_imgu' typeof_fun 𝒱 term1 term2 μ"
    using welltyped_imgu'_exists
    by meson

  let ?conclusion' = "add_mset (term1 ≈ term2') (add_mset (term1' !≈ term2') premise')"

  have eq_factoring: "eq_factoring (premise, 𝒱) (?conclusion' ⋅ μ, 𝒱)"
  proof (rule eq_factoringI)
    show "premise = add_mset literal1 (add_mset literal2 premise')"
      using premise.
  next
    show "literal1 = term1 ≈ term1'"
      using literal1_terms.
  next 
    show "literal2 = term2 ≈ term2'"
      using literal2_terms.
  next 
    show  "select premise = {#}"
      using select_empty.
  next
    have literal1_μ_in_premise: "literal1 ⋅l μ ∈# premise ⋅ μ"
      using literal1_maximal(1) clause.subst_in_to_set_subst maximall_in_clause by blast

    have "is_maximall (literal1 ⋅l μ) (premise ⋅ μ)"
      using is_maximall_ground_subst_stability'[OF 
          literal1_μ_in_premise 
          premise_grounding[unfolded μ(2) clause.subst_comp_subst]
          literal1_maximal(2)[unfolded μ(2) clause.subst_comp_subst literal.subst_comp_subst]
          ].

    then show "is_maximall (literal1 ⋅l μ) (premise ⋅ μ)"
      by blast
  next
    have term_groundings: "term.is_ground (term1' ⋅t μ ⋅t σ)" "term.is_ground (term1 ⋅t μ ⋅t σ)" 
      unfolding 
        term_subst.subst_comp_subst[symmetric] 
        μ(2)[symmetric]
        termG1_term1[symmetric] 
        termG2_term1'[symmetric] 
      using term.ground_is_ground
      by simp_all

    have "term1' ⋅t μ ⋅t σ ≺t term1 ⋅t μ ⋅t σ"
      using ground_eq_factoringI(6)[unfolded 
          lesstG_def 
          termG1_term1 
          termG2_term1'
          μ(2) 
          term_subst.subst_comp_subst
          ].

    then show "¬ term1 ⋅t μ ≼t term1' ⋅t μ"
      using lesst_less_eqt_ground_subst_stability[OF term_groundings]
      by blast
  next 
    show "term_subst.is_imgu μ {{term1, term2}}"
      using μ(1).
  next 
    show "welltyped_imgu' typeof_fun 𝒱 term1 term2 μ"
      using μ(3).
  next
    show "?conclusion' ⋅ μ = ?conclusion' ⋅ μ"
      ..
  qed

  have "term_subst.is_idem μ"
    using μ(1)
    by (simp add: term_subst.is_imgu_iff_is_idem_and_is_mgu)  

  then have μ_γ: "μ ⊙ γ = γ"
    unfolding μ(2) term_subst.is_idem_def
    by (metis subst_compose_assoc)

  have vars_conclusion': "clause.vars (?conclusion' ⋅ μ) ⊆ clause.vars premise"
    using vars_clause_imgu[OF μ(1)] vars_term_imgu[OF μ(1)]
    unfolding premise literal1_terms literal2_terms
    by clause_auto

  have "conclusion ⋅ γ = 
      add_mset (term.from_ground termG2 !≈ term.from_ground termG3) 
        (add_mset (term.from_ground termG1 ≈ term.from_ground termG3) (clause.from_ground premise'G))"
    using ground_eq_factoringI(7) clause.to_ground_inverse[OF conclusion_grounding]
    unfolding atom_from_ground_term_from_ground[symmetric] 
      literal_from_ground_atom_from_ground[symmetric] clause_from_ground_add_mset[symmetric]
    by simp

  then have conclusion_γ: 
    "conclusion ⋅ γ = add_mset (term1 ≈ term2') (add_mset (term1' !≈ term2') premise') ⋅ γ"
    unfolding 
      termG2_term1'
      termG3_term2'
      termG1_term1
      premise'_γ[symmetric]
    by(clause_simp simp: add_mset_commute)

  then have "?conclusion' ⋅ μ ⋅ γ = conclusion ⋅ γ"
    by (metis μ_γ clause.subst_comp_subst)

  moreover have 
    "Infer [premiseG] conclusionG ∈ inference_groundings (Infer [(premise, 𝒱)] (?conclusion' ⋅ μ, 𝒱))"
    unfolding inference_groundings_def mem_Collect_eq
  proof -
    have "Infer [premiseG] conclusionG ∈ ground.G_Inf"
      unfolding ground.G_Inf_def
      using ground_eq_factoring conclusion_grounding premise_grounding 
      by blast

    then have "∃ρ1 ρ2. is_inference_grounding
      (Infer [(premise, 𝒱)] (?conclusion' ⋅ μ, 𝒱))
      (Infer [premiseG] conclusionG) γ ρ1 ρ2"
      unfolding is_inference_grounding_def Calculus.inference.case list.case prod.case
      using typing
      by (smt (verit) calculation conclusionG eq_factoring eq_factoring_preserves_typing premiseG
          vars_conclusion' welltypedσ_on_subset)

    thus "∃ιG γ ρ1 ρ2. Infer [premiseG] conclusionG = ιG ∧
      is_inference_grounding (Infer [(premise, 𝒱)] (?conclusion' ⋅ μ, 𝒱)) ιG γ ρ1 ρ2"
      by iprover
  qed    

  ultimately show ?thesis
    using that[OF eq_factoring]
    by blast
qed



lemma if_subst_sth [clause_simp]: "(if b then Pos else Neg) atom ⋅l ρ = 
  (if b then Pos else Neg) (atom ⋅a ρ)"
  by clause_auto

lemma superposition_lifting:
  fixes 
    premiseG1 premiseG2 conclusionG :: "'f gatom clause" and 
    premise1 premise2 "conclusion" :: "('f, 'v) atom clause" and
    γ ρ1 ρ2 :: "('f, 'v) subst" and
    𝒱1 𝒱2
  defines 
    premiseG1 [simp]: "premiseG1 ≡ clause.to_ground (premise1 ⋅ ρ1 ⋅ γ)" and
    premiseG2 [simp]: "premiseG2 ≡ clause.to_ground (premise2 ⋅ ρ2 ⋅ γ)" and
    conclusionG [simp]: "conclusionG ≡ clause.to_ground (conclusion ⋅ γ)" and
    premise_groundings [simp]: 
    "premise_groundings ≡ clause_groundings typeof_fun (premise1, 𝒱1) ∪ 
      clause_groundings typeof_fun (premise2, 𝒱2)" and
    ιG [simp]: "ιG ≡ Infer [premiseG2, premiseG1] conclusionG"
  assumes 
    renaming: 
    "term_subst.is_renaming ρ1" 
    "term_subst.is_renaming ρ2" 
    "clause.vars (premise1 ⋅ ρ1) ∩ clause.vars (premise2 ⋅ ρ2) = {}"  and
    premise1_grounding: "clause.is_ground (premise1 ⋅ ρ1 ⋅ γ)" and
    premise2_grounding: "clause.is_ground (premise2 ⋅ ρ2 ⋅ γ)" and
    conclusion_grounding: "clause.is_ground (conclusion ⋅ γ)" and
    select: 
    "clause.from_ground (selectG premiseG1) = (select premise1) ⋅ ρ1 ⋅ γ"
    "clause.from_ground (selectG premiseG2) = (select premise2) ⋅ ρ2 ⋅ γ" and
    ground_superposition: "ground.ground_superposition premiseG2 premiseG1 conclusionG" and
    non_redundant: "ιG ∉ ground.Red_I premise_groundings" and
    typing:
    "welltypedc typeof_fun 𝒱1 premise1"
    "welltypedc typeof_fun 𝒱2 premise2"
    "term_subst.is_ground_subst γ"
    "welltypedσ_on (clause.vars premise1) typeof_fun 𝒱1 (ρ1 ⊙ γ)"
    "welltypedσ_on (clause.vars premise2) typeof_fun 𝒱2 (ρ2 ⊙ γ)"
    "welltypedσ_on (clause.vars premise1) typeof_fun 𝒱1 ρ1"
    "welltypedσ_on (clause.vars premise2) typeof_fun 𝒱2 ρ2"
    "all_types 𝒱1" "all_types 𝒱2"
  obtains conclusion' 𝒱3
  where
    "superposition (premise2, 𝒱2) (premise1, 𝒱1) (conclusion', 𝒱3)"
    "ιG ∈ inference_groundings (Infer [(premise2, 𝒱2), (premise1, 𝒱1)] (conclusion', 𝒱3))"
    "conclusion' ⋅ γ = conclusion ⋅ γ"
  using ground_superposition
proof(cases premiseG2 premiseG1 conclusionG rule: ground.ground_superposition.cases)
  case (ground_superpositionI 
      literalG1
      premiseG1'
      literalG2
      premiseG2'
      𝒫G
      contextG
      termG1
      termG2
      termG3
      )

  have premise1_not_empty: "premise1 ≠ {#}"
    using ground_superpositionI(1) empty_not_add_mset clause_subst_empty premiseG1
    by (metis clause_from_ground_empty_mset clause.from_ground_inverse)

  have premise2_not_empty: "premise2 ≠ {#}"
    using ground_superpositionI(2) empty_not_add_mset clause_subst_empty premiseG2
    by (metis clause_from_ground_empty_mset clause.from_ground_inverse)

  have premise1_γ: "premise1 ⋅ ρ1 ⋅ γ = clause.from_ground (add_mset literalG1 premiseG1')"
    using ground_superpositionI(1) premiseG1
    by (metis premise1_grounding clause.to_ground_inverse)

  have premise2_γ: "premise2 ⋅ ρ2 ⋅ γ = clause.from_ground (add_mset literalG2 premiseG2')"
    using ground_superpositionI(2) premiseG2
    by (metis premise2_grounding clause.to_ground_inverse)

  let ?selectG_empty = "selectG (clause.to_ground (premise1 ⋅ ρ1 ⋅ γ)) = {#}"
  let ?selectG_not_empty = "selectG (clause.to_ground (premise1 ⋅ ρ1 ⋅ γ)) ≠ {#}"

  have pos_literalG1_is_strictly_maximall: 
    "is_strictly_maximall (literal.from_ground literalG1) (premise1 ⋅ ρ1 ⊙ γ)" if "𝒫G = Pos"
    using ground_superpositionI(9) that
    unfolding is_strictly_maximalGl_iff_is_strictly_maximall
    by(simp add: premise1_grounding)

  have neg_literalG1_is_maximall: 
    "is_maximall (literal.from_ground literalG1) (premise1 ⋅ ρ1 ⊙ γ)" if ?selectG_empty
    using 
      that
      ground_superpositionI(9)  
      is_maximall_if_is_strictly_maximall 
      is_maximall_empty
      premise1_γ
    unfolding 
      is_maximal_lit_iff_is_maximall 
      is_strictly_maximalGl_iff_is_strictly_maximall
      ground_superpositionI(1)
    apply clause_auto
    by (metis premise1_γ clause_from_ground_empty_mset clause.from_ground_inverse)

  obtain pos_literal1 where
    "is_strictly_maximall pos_literal1 premise1"
    "pos_literal1 ⋅l ρ1 ⊙ γ = literal.from_ground literalG1" 
  if "𝒫G = Pos"
    using is_strictly_maximall_ground_subst_stability[OF 
        premise1_grounding[folded clause.subst_comp_subst] 
        pos_literalG1_is_strictly_maximall
        ]
    by blast

  moreover then have "pos_literal1 ∈# premise1" if "𝒫G = Pos"
    using that strictly_maximall_in_clause by fastforce

  moreover obtain neg_max_literal1 where
    "is_maximall neg_max_literal1 premise1"
    "neg_max_literal1 ⋅l ρ1 ⊙ γ = literal.from_ground literalG1" 
  if "𝒫G = Neg" ?selectG_empty
    using 
      is_maximall_ground_subst_stability[OF 
        premise1_not_empty 
        premise1_grounding[folded clause.subst_comp_subst]
        ]
      neg_literalG1_is_maximall
    by (metis (no_types, opaque_lifting) assms(9) clause.comp_subst.left.monoid_action_compatibility unique_maximal_in_ground_clause)

  moreover then have "neg_max_literal1 ∈# premise1" if "𝒫G = Neg" ?selectG_empty
    using that maximall_in_clause by fastforce

  moreover obtain neg_selected_literal1 where
    "is_maximall neg_selected_literal1 (select premise1)"
    "neg_selected_literal1 ⋅l ρ1 ⊙ γ = literal.from_ground literalG1" 
  if "𝒫G = Neg" ?selectG_not_empty 
  proof-
    have "ground.is_maximal_lit literalG1 (selectG premiseG1)" if "𝒫G = Neg" ?selectG_not_empty
      using ground_superpositionI(9) that
      by simp

    then show ?thesis
      using
        that 
        select(1) 
        unique_maximal_in_ground_clause
        is_maximall_ground_subst_stability
      unfolding premiseG1 is_maximal_lit_iff_is_maximall
      by (metis (mono_tags, lifting) clause.comp_subst.monoid_action_compatibility 
          clause_subst_empty(2) clause.ground_is_ground image_mset_is_empty_iff 
          clause.from_ground_def)
  qed

  moreover then have "neg_selected_literal1 ∈# premise1" if "𝒫G = Neg" ?selectG_not_empty 
    using that
    by (meson maximall_in_clause mset_subset_eqD select_subset)

  ultimately obtain literal1 where
    literal1_γ: "literal1 ⋅l ρ1 ⊙ γ = literal.from_ground literalG1" and
    literal1_in_premise1: "literal1 ∈# premise1" and
    literal1_is_strictly_maximal: "𝒫G = Pos ⟹ is_strictly_maximall literal1 premise1" and
    literal1_is_maximal: "𝒫G = Neg ⟹ ?selectG_empty ⟹ is_maximall literal1 premise1" and
    literal1_selected: "𝒫G = Neg ⟹ ?selectG_not_empty ⟹ is_maximall literal1 (select premise1)"
    by (metis ground_superpositionI(9) literals_distinct(1))

  then have literal1_grounding: "literal.is_ground (literal1 ⋅l ρ1 ⊙ γ)"
    by simp

  have literalG2_is_strictly_maximall: 
    "is_strictly_maximall (literal.from_ground literalG2) (premise2 ⋅ ρ2 ⊙ γ)"
    using ground_superpositionI(11)
    unfolding is_strictly_maximalGl_iff_is_strictly_maximall
    by (simp add: premise2_grounding)

  obtain literal2 where 
    literal2_strictly_maximal: "is_strictly_maximall literal2 premise2" and
    literal2_γ: "literal2 ⋅l ρ2 ⊙ γ = literal.from_ground literalG2"
    using is_strictly_maximall_ground_subst_stability[OF 
        premise2_grounding[folded clause.subst_comp_subst] 
        literalG2_is_strictly_maximall
        ].

  then have literal2_in_premise2: "literal2 ∈# premise2" 
    using strictly_maximall_in_clause by blast

  have literal2_grounding: "literal.is_ground (literal2 ⋅l ρ2 ⊙ γ)"
    using literal2_γ by simp

  obtain premise1' where premise1: "premise1 = add_mset literal1 premise1'"
    by (meson literal1_in_premise1 multi_member_split)

  then have premise1'_γ: "premise1' ⋅ ρ1 ⋅ γ = clause.from_ground premiseG1'"
    using premise1_γ  
    unfolding clause_from_ground_add_mset literal1_γ[symmetric]
    by (simp add: subst_clause_add_mset)

  obtain premise2' where premise2: "premise2 = add_mset literal2 premise2'"
    by (meson literal2_in_premise2 multi_member_split)

  then have premise2'_γ: "premise2' ⋅ ρ2 ⋅ γ = clause.from_ground premiseG2'"
    using premise2_γ  
    unfolding clause_from_ground_add_mset literal2_γ[symmetric]
    by (simp add: subst_clause_add_mset)

  let ?𝒫 = "if 𝒫G = Pos then Pos else Neg"

  have [simp]: "𝒫G ≠ Pos ⟷ 𝒫G = Neg"
    using ground_superpositionI(4) 
    by auto

  have "literal1 ⋅l ρ1 ⋅l γ = 
    ?𝒫 (Upair (context.from_ground contextG)⟨term.from_ground termG1⟩ (term.from_ground termG2))"
    using literal1_γ
    unfolding ground_superpositionI(5)
    by (simp add: literal_from_ground_atom_from_ground atom_from_ground_term_from_ground 
        ground_term_with_context(3))

  then obtain term1_with_context term1' where 
    literal1: "literal1 = ?𝒫 (Upair term1_with_context term1')" and
    term1'_γ: "term1' ⋅t ρ1 ⋅t γ = term.from_ground termG2" and
    term1_with_context_γ: 
      "term1_with_context ⋅t ρ1 ⋅t γ = (context.from_ground contextG)⟨term.from_ground termG1⟩"
    by (smt (verit) obtain_from_literal_subst)

  from literal2_γ have "literal2 ⋅l ρ2 ⋅l γ = term.from_ground termG1 ≈ term.from_ground termG3"
    unfolding ground_superpositionI(6) atom_from_ground_term_from_ground 
      literal_from_ground_atom_from_ground(2) literal.subst_comp_subst.

  then obtain term2 term2' where 
    literal2: "literal2 = term2 ≈ term2'" and
    term2_γ: "term2 ⋅t ρ2 ⋅t γ = term.from_ground termG1" and     
    term2'_γ: "term2' ⋅t ρ2 ⋅t γ = term.from_ground termG3"
    using obtain_from_pos_literal_subst
    by metis

  let ?inference_into_var = "∄context1 term1. 
      term1_with_context = context1⟨term1⟩ ∧ 
      term1 ⋅t ρ1 ⋅t γ = term.from_ground termG1 ∧ 
      context1 ⋅tc ρ1 ⋅tc γ = context.from_ground contextG ∧ 
      is_Fun term1"

  have inference_into_var_is_redundant: 
    "?inference_into_var ⟹ ground.redundant_infer premise_groundings ιG"
  proof-
    assume inference_into_var: ?inference_into_var

    obtain termx contextx contextx' where
      term1_with_context: "term1_with_context = contextx⟨termx⟩" and
      is_Var_termx: "is_Var termx" and
      "context.from_ground contextG = (contextx ⋅tc ρ1 ⋅tc γ) ∘c contextx'"
    proof-  
      from inference_into_var term1_with_context_γ
      have 
        "∃termx contextx contextx'. 
        term1_with_context = contextx⟨termx⟩ ∧ 
        is_Var termx ∧ 
        context.from_ground contextG = (contextx ⋅tc ρ1 ⋅tc γ) ∘c contextx'"
      proof(induction term1_with_context arbitrary: contextG)
        case (Var x)
        show ?case
        proof(intro exI conjI)
          show
            "Var x = □⟨Var x⟩"
            "is_Var (Var x)"
            "context.from_ground contextG = (□ ⋅tc ρ1 ⋅tc γ) ∘c context.from_ground contextG"
            by simp_all
        qed
      next
        case (Fun f terms)

        then have "contextG ≠ GHole"
          by (metis ctxt_of_gctxt.simps(1) vars_term_of_gterm
              vars_ctxt_of_gctxt[of "gctxt_of_ctxt (□ ∘c □)"]
              gctxt_ident_iff_eq_GHole[of "□G" termG1]
              gctxt_ident_iff_eq_GHole[of "□G" undefined]
              ctxt_eq[of "□" "Fun f terms" "□⟨Fun f terms⟩"]
              ground_term_with_context3[of contextG termG1]
              ground_term_with_context3[of "□G" undefined]
              actxt.map(1)[of "λx. x" "λuua. uua ⋅t ρ1"]
              actxt.map(1)[of "λx. x" "λuua. uua ⋅t γ"]
              intp_actxt_compose[of Fun "□" "□" "Fun f terms"]
              intp_actxt_compose[of Fun "□" "□" "term_of_gterm undefined"]
              gctxt_of_ctxt_inv[of "□ ∘c □"]
              term.discI(2)[of "Fun f terms" f terms]
              lesst_ground_subterm_property[of "term.from_ground undefined" "□ ∘c □"]
              term_of_gterm_ctxt_apply_ground(1)[of undefined "□ ∘c □" "term_of_gterm undefined"]
              term_order.less_imp_not_eq[of "term.from_ground _" "term.from_ground _"])

        then obtain termsG1 contextG' termsG2 where
          contextG: "contextG = GMore f termsG1 contextG' termsG2"
          using Fun(3)
          by(cases contextG) auto

        have terms_γ: 
          "map (λterm. term ⋅t ρ1 ⋅t γ) terms = 
            map term.from_ground termsG1 @ (context.from_ground contextG')⟨term.from_ground termG1⟩ #
             map term.from_ground termsG2"
          using Fun(3)
          unfolding contextG
          by(simp add: comp_def)

        then obtain terms1 "term" terms2 where 
          terms: "terms = terms1 @ term # terms2" and
          terms1_γ: "map (λterm. term ⋅t ρ1 ⋅t γ) terms1 = map term.from_ground termsG1" and
          terms2_γ: "map (λterm. term ⋅t ρ1 ⋅t γ) terms2 = map term.from_ground termsG2"     
          by (smt (z3) append_eq_map_conv map_eq_Cons_D)

        with terms_γ 
        have term_γ: "term ⋅t ρ1 ⋅t γ = (context.from_ground contextG')⟨term.from_ground termG1⟩"
          by simp

        show ?case
        proof(cases "term.is_ground term")
          case True

          with term_γ 
          obtain term1 context1 where
            "term = context1⟨term1⟩"
            "term1 ⋅t ρ1 ⋅t γ = term.from_ground termG1" 
            "context1 ⋅tc ρ1 ⋅tc γ = context.from_ground contextG'" 
            "is_Fun term1"
            by (metis Term.ground_vars_term_empty context.ground_is_ground ground_subst_apply 
                term.ground_is_ground context.subst_ident_if_ground gterm_is_fun)

          moreover then have "Fun f terms = (More f terms1 context1 terms2)⟨term1⟩"
            unfolding terms
            by auto

          ultimately have 
            "∃context1 term1. 
            Fun f terms = context1⟨term1⟩ ∧ 
            term1 ⋅t ρ1 ⋅t γ = term.from_ground termG1 ∧ 
            context1 ⋅tc ρ1 ⋅tc γ = context.from_ground contextG ∧ 
            is_Fun term1"
            by (auto
                intro: exI[of _ "More f terms1 context1 terms2"] exI[of _ term1] 
                simp: comp_def terms1_γ terms2_γ contextG)

          then show ?thesis
            using Fun(2)
            by argo
        next
          case False
          moreover have "term ∈ set terms"
            using terms by auto

          moreover have 
            "∄context1 term1. term = context1⟨term1⟩ ∧ 
            term1 ⋅t ρ1 ⋅t γ = term.from_ground termG1 ∧ 
            context1 ⋅tc ρ1 ⋅tc γ = context.from_ground contextG' ∧ 
            is_Fun term1"
          proof(rule notI)
            assume 
              "∃context1 term1. 
              term = context1⟨term1⟩ ∧ 
              term1 ⋅t ρ1 ⋅t γ = term.from_ground termG1 ∧ 
              context1 ⋅tc ρ1 ⋅tc γ = context.from_ground contextG' ∧ 
              is_Fun term1"

            then obtain context1 term1 where
              "term": "term = context1⟨term1⟩"
              "term1 ⋅t ρ1 ⋅t γ = term.from_ground termG1"
              "context1 ⋅tc ρ1 ⋅tc γ = context.from_ground contextG'"
              "is_Fun term1"
              by blast

            then have 
              "∃context1 term1. 
              Fun f terms = context1⟨term1⟩ ∧ 
              term1 ⋅t ρ1 ⋅t γ = term.from_ground termG1 ∧ 
              context1 ⋅tc ρ1 ⋅tc γ = context.from_ground contextG ∧ 
              is_Fun term1"
              by(auto 
                  intro: exI[of _ "(More f terms1 context1 terms2)"] exI[of _ term1] 
                  simp: "term" terms terms1_γ terms2_γ contextG comp_def)

            then show False
              using Fun(2)
              by argo
          qed

          ultimately obtain termx contextx contextx' where
            "term = contextx⟨termx⟩"  
            "is_Var termx" 
            "context.from_ground contextG' = (contextx ⋅tc ρ1 ⋅tc γ) ∘c contextx'"
            using Fun(1) term_γ by blast

          then have 
            "Fun f terms = (More f terms1 contextx terms2)⟨termx⟩"
            "is_Var termx" 
            "context.from_ground contextG = (More f terms1 contextx terms2 ⋅tc ρ1 ⋅tc γ) ∘c contextx'"
            by(auto simp: terms terms1_γ terms2_γ contextG comp_def)

          then show ?thesis
            by blast
        qed
      qed

      then show ?thesis
        using that
        by blast
    qed

    then have contextG: "context.from_ground contextG = contextx ∘c contextx' ⋅tc ρ1 ⋅tc γ"
      using ground_context_subst[OF context.ground_is_ground] ctxt_compose_subst_compose_distrib
      by metis

    obtain τx where τx: "welltyped typeof_fun 𝒱1 termx τx"
      using term1_with_context typing(1)
      unfolding premise1 welltypedc_def literal1 welltypedl_def welltypeda_def
      by (metis welltyped.simps is_Var_termx term.collapse(1))
 
    have ιG_parts: 
      "set (side_prems_of ιG) = {premiseG2}" 
      "main_prem_of ιG = premiseG1"
      "concl_of ιG = conclusionG"
      unfolding ιG
      by simp_all

    from is_Var_termx 
    obtain varx where varx: "Var varx = termx ⋅t ρ1"
      using renaming(1)[unfolded term_subst_is_renaming_iff]
      by (cases termx) auto

    have τx_varx: "welltyped typeof_fun 𝒱1 (Var varx) τx"
      using τx typing(6)
      unfolding welltypedσ_on_def varx premise1 literal1 term1_with_context 
      by(clause_auto simp: welltypedσ_on_def welltypedσ_on_welltyped)

    show ?thesis
    proof(unfold ground.redundant_infer_def ιG_parts, intro exI conjI)

      let ?update = "(contextx' ⋅tc ρ1 ⋅tc γ)⟨term.from_ground termG3⟩"

      define γ' where
        γ': "γ' ≡ γ(varx := ?update)"

      have update_grounding: "term.is_ground ?update"
      proof-
        have "context.is_ground ((contextx ⋅tc ρ1 ⋅tc γ) ∘c (contextx' ⋅tc ρ1 ⋅tc γ))"
          using context.ground_is_ground[of contextG] contextG
          by fastforce

        then show ?thesis
          using context_is_ground_context_compose1(2)
          by auto
      qed
      let ?contextx'_γ = "context.to_ground (contextx' ⋅tc ρ1 ⋅tc γ)"

      note term_from_ground_context =
        ground_term_with_context1[OF _ term.ground_is_ground, unfolded term.from_ground_inverse]

      have termx_γ: "term.to_ground (termx ⋅t ρ1 ⋅t γ) = ?contextx'_γ⟨termG1⟩G"
        using term1_with_context_γ update_grounding 
        unfolding term1_with_context contextG
        by(auto simp: term_from_ground_context)

      have termx_γ': "term.to_ground (termx ⋅t ρ1 ⋅t γ') = ?contextx'_γ⟨termG3⟩G"
        using update_grounding
        unfolding varx[symmetric] γ'
        by(auto simp: term_from_ground_context)

      have aux: "termx ⋅t ρ1 ⋅t γ = (contextx' ⋅tc ρ1 ⋅tc γ)⟨term.from_ground termG1⟩"
        using termx_γ
        by (metis ground_term_with_context2 term_subst.is_ground_subst_is_ground 
            term_with_context_is_ground term.to_ground_inverse typing(3) update_grounding)

      have "welltypedc typeof_fun 𝒱2 (clause.from_ground premiseG2)"
        by (metis ground_superpositionI(2) premise2_γ 
            clause.comp_subst.left.monoid_action_compatibility typing(2) typing(5) 
            welltypedσ_on_welltypedc)

      then have "∃τ. welltyped typeof_fun 𝒱2 (term.from_ground termG1) τ ∧ 
          welltyped typeof_fun 𝒱2 (term.from_ground termG3) τ"
        unfolding ground_superpositionI 
        by clause_simp

      then have aux': "∃τ. welltyped typeof_fun 𝒱1 (term.from_ground termG1) τ ∧ 
          welltyped typeof_fun 𝒱1 (term.from_ground termG3) τ"
        by (meson term.ground_is_ground welltyped_is_ground)

      have "welltyped typeof_fun 𝒱1 (termx ⋅t ρ1 ⋅t γ) τx"
      proof-

        have "
          ⟦∀x∈context.vars contextx ∪ term.vars termx ∪ term.vars term1' ∪ clause.vars premise1'.
            First_Order_Type_System.welltyped typeof_fun 𝒱1 ((ρ1 ⊙ γ) x) (𝒱1 x);
            First_Order_Type_System.welltyped typeof_fun 𝒱1 termx τx⟧
            ⟹ First_Order_Type_System.welltyped typeof_fun 𝒱1 (termx ⋅t ρ1 ⋅t γ) τx"
          by (metis UnI2 sup.commute term_subst.subst_comp_subst welltypedσ_on_def welltypedσ_on_term)
        
        then show ?thesis
          using typing(4) τx
          unfolding welltypedσ_on_def varx premise1 literal1 term1_with_context 
          by clause_simp
      qed

      then have τx_update: "welltyped typeof_fun 𝒱1 ?update τx"
        unfolding aux
        using aux'
        by (meson welltypedκ)

      let ?premise1_γ' = "clause.to_ground (premise1 ⋅ ρ1 ⋅ γ')"
      have premise1_γ'_grounding: "clause.is_ground (premise1 ⋅ ρ1 ⋅ γ')"
        using clause.ground_subst_upd[OF update_grounding premise1_grounding] 
        unfolding γ'
        by blast

      have γ'_ground: "term_subst.is_ground_subst (ρ1 ⊙ γ')"
        by (metis γ' term.ground_subst_upd term_subst.comp_subst.left.monoid_action_compatibility 
            term_subst.is_ground_subst_def typing(3) update_grounding)

      have γ'_wt: "welltypedσ_on (clause.vars premise1) typeof_fun 𝒱1 (ρ1 ⊙ γ')"
        using welltypedσ_on_subst_upd[OF τx_varx τx_update typing(4)]
        unfolding γ' welltypedσ_on_def subst_compose
        using First_Order_Type_System.welltyped.simps τx τx_update eval_term.simps(1) 
          eval_with_fresh_var fun_upd_same is_Var_termx renaming(1) subst_compose_def 
          term.collapse(1) term.distinct(1) term.set_cases(2) term_subst_is_renaming_iff 
          the_inv_f_f typing(4) varx welltypedσ_on_def
        by (smt (verit, del_insts))
      
      show "{?premise1_γ'} ⊆ premise_groundings"
        using premise1_γ'_grounding typing γ'_wt γ'_ground
        unfolding clause.subst_comp_subst[symmetric] premise1 premise_groundings 
          clause_groundings_def
        by auto

      show "finite {?premise1_γ'}"
        by simp

      show "ground.G_entails ({?premise1_γ'} ∪ {premiseG2}) {conclusionG}"
      proof(unfold ground.G_entails_def, intro allI impI)
        fix I :: "'f gterm rel"
        let ?I = "upair ` I"

        assume 
          refl: "refl I" and 
          trans: "trans I" and 
          sym: "sym I" and
          compatible_with_gctxt: "compatible_with_gctxt I" and
          premise: "?I ⊫s {?premise1_γ'} ∪ {premiseG2}"

        have varx_γ_ground: "term.is_ground (Var varx ⋅t γ)"
          using term1_with_context_γ
          unfolding term1_with_context varx
          by(clause_simp simp: term_subst.is_ground_subst_is_ground typing(3))    

        show "?I ⊫s { conclusionG }"
        proof(cases "?I ⊫ premiseG2'")
          case True
          then show ?thesis 
            unfolding ground_superpositionI(12)
            by auto
        next
          case False
          then have literalG2: "?I ⊫l literalG2"
            using premise 
            unfolding ground_superpositionI(2)
            by blast

          then have "?I ⊫l ?contextx'_γ⟨termG1⟩G ≈ ?contextx'_γ⟨termG3⟩G"
            unfolding ground_superpositionI(6)
            using compatible_with_gctxt compatible_with_gctxt_def sym 
            by auto

          then have "?I ⊫l term.to_ground (termx ⋅t ρ1 ⋅t γ) ≈ term.to_ground (termx ⋅t ρ1 ⋅t γ')"
            using termx_γ termx_γ'
            by argo

          moreover then have "?I ⊫ ?premise1_γ'"
            using premise by fastforce

          ultimately have "?I ⊫ premiseG1"
            using
              interpretation_clause_congruence[OF 
                trans sym compatible_with_gctxt update_grounding varx_γ_ground premise1_grounding
                ]
              varx
            unfolding γ'
            by simp

          then have "?I ⊫ add_mset (𝒫G (Upair contextG⟨termG1⟩G termG2)) premiseG1'"
            using ground_superpositionI(1) ground_superpositionI(5) by auto

          then have "?I ⊫ add_mset (𝒫G (Upair contextG⟨termG3⟩G termG2)) premiseG1'"
            using 
              literalG2
              interpretation_context_congruence[OF trans sym compatible_with_gctxt]
              interpretation_context_congruence'[OF trans sym compatible_with_gctxt]
              ground_superpositionI(4)
            unfolding ground_superpositionI(6)
            by(cases "𝒫G = Pos")(auto simp: sym)

          then show ?thesis 
            unfolding ground_superpositionI(12)
            by blast
        qed
      qed

      show "∀clauseG ∈ {?premise1_γ'}. clauseG ≺cG premiseG1"
      proof-
        have varx_γ: "γ varx = termx ⋅t ρ1 ⋅t γ"
          using varx
          by simp

        have contextx_grounding: "context.is_ground (contextx ⋅tc ρ1 ⋅tc γ)"
          using contextG
          unfolding subst_compose_ctxt_compose_distrib
          by (metis context.ground_is_ground context_is_ground_context_compose1(1))

        have termx_grounding: "term.is_ground (termx ⋅t ρ1 ⋅t γ)"
          using term1_with_context_γ
          unfolding term1_with_context
          by(clause_simp simp: term_subst.is_ground_subst_is_ground typing(3))

        have 
          "(contextx ∘c contextx' ⋅tc ρ1 ⋅tc γ)⟨term.from_ground termG3⟩ ≺t contextx⟨termx⟩ ⋅t ρ1 ⋅t γ"
          using ground_superpositionI(8)
          unfolding 
            lesstG_def 
            contextG[symmetric] 
            term1_with_context[symmetric] 
            term1_with_context_γ
            lesst_ground_context_compatible_iff[OF 
              context.ground_is_ground term.ground_is_ground term.ground_is_ground].

        then have update_smaller: "?update ≺t γ varx"
          unfolding 
            varx_γ
            subst_apply_term_ctxt_apply_distrib 
            subst_compose_ctxt_compose_distrib
            Subterm_and_Context.ctxt_ctxt_compose
          by(rule lesst_ground_context_compatible'[OF 
                contextx_grounding update_grounding termx_grounding])     

        have varx_in_literal1: "varx ∈ literal.vars (literal1 ⋅l ρ1)"
          unfolding literal1 term1_with_context literal.vars_def atom.vars_def 
          using varx
          by(auto simp: subst_literal subst_atom)

        have literal1_smaller: "literal1 ⋅l ρ1 ⋅l γ' ≺l literal1 ⋅l ρ1 ⋅l γ"
          unfolding γ'
          using lessl_subst_upd[OF 
              update_grounding 
              update_smaller 
              literal1_grounding[unfolded literal.subst_comp_subst] 
              varx_in_literal1
              ].

        have premise1'_grounding: "clause.is_ground (premise1' ⋅ ρ1 ⋅ γ)"
          using premise1'_γ
          by simp

        have premise1'_smaller: "premise1' ⋅ ρ1 ⋅ γ' ≼c premise1' ⋅ ρ1 ⋅ γ"
          unfolding γ'
          using lessc_subst_upd[of _ γ, OF update_grounding update_smaller premise1'_grounding]
          by(cases "varx ∈ clause.vars (premise1' ⋅ ρ1)") simp_all

        have "?premise1_γ' ≺cG premiseG1"
          using lessc_add_mset[OF literal1_smaller premise1'_smaller]
          unfolding 
            lesscG_lessc 
            premiseG1
            subst_clause_add_mset[symmetric]
            clause.to_ground_inverse[OF premise1_γ'_grounding]
            clause.to_ground_inverse[OF premise1_grounding]
          unfolding premise1.

        then show ?thesis
          by blast
      qed   
    qed
  qed

  obtain context1 term1 where 
    term1_with_context: "term1_with_context = context1⟨term1⟩" and
    term1_γ: "term1 ⋅t ρ1 ⋅t γ = term.from_ground termG1" and
    context1_γ: "context1 ⋅tc ρ1 ⋅tc γ = context.from_ground contextG" and
    term1_not_Var: "¬ is_Var term1"
    using non_redundant ground_superposition inference_into_var_is_redundant 
    unfolding
      ground.Red_I_def 
      ground.G_Inf_def 
      premise_groundings 
      ιG 
      conclusionG 
      ground_superpositionI(1, 2) 
      premise_groundings 
    by blast

  obtain term2'_with_context where 
    term2'_with_context_γ: 
      "term2'_with_context ⋅t γ = (context.from_ground contextG)⟨term.from_ground termG3⟩" and
    term2'_with_context: "term2'_with_context = (context1 ⋅tc ρ1)⟨term2' ⋅t ρ2⟩" 
    unfolding term2'_γ[symmetric] context1_γ[symmetric]
    by force

  define 𝒱3 where 
    "⋀x. 𝒱3 x ≡
        if x ∈ clause.vars (premise1 ⋅ ρ1)
        then 𝒱1 (the_inv ρ1 (Var x))
        else 𝒱2 (the_inv ρ2 (Var x))"

  have wt_γ: 
    "welltypedσ_on (clause.vars (premise1 ⋅ ρ1) ∪ clause.vars (premise2 ⋅ ρ2)) typeof_fun 𝒱3 γ"
  proof(unfold welltypedσ_on_def, intro ballI)
    fix x
    assume x_in_vars: "x ∈ clause.vars (premise1 ⋅ ρ1) ∪ clause.vars (premise2 ⋅ ρ2)"

    obtain f ts where γ_x: "γ x = Fun f ts"
      using obtain_ground_fun term_subst.is_ground_subst_is_ground[OF typing(3)]
      by (metis eval_term.simps(1))

    have "welltyped typeof_fun 𝒱3 (γ x) (𝒱3 x)"
    proof(cases "x ∈ clause.vars (premise1 ⋅ ρ1)")
      case True
      then have "Var x ∈ ρ1 ` clause.vars premise1"
        by (metis image_eqI renaming(1) renaming_vars_clause)

      then have y_in_vars: "the_inv ρ1 (Var x) ∈ clause.vars premise1"
        by (metis (no_types, lifting) image_iff renaming(1) term_subst_is_renaming_iff the_inv_f_f)

      define y where "y ≡ the_inv ρ1 (Var x)"

      have "term.is_ground (Var y ⋅t ρ1 ⋅t γ)"
        using term_subst.is_ground_subst_is_ground typing(3) by blast

      moreover have "welltyped typeof_fun 𝒱1 (Var y ⋅t ρ1 ⋅t γ) (𝒱1 y)"
        using typing(4) y_in_vars
        unfolding welltypedσ_on_def y_def
        by (simp add: subst_compose)

      ultimately have "welltyped typeof_fun 𝒱3 (Var y ⋅t ρ1 ⋅t γ) (𝒱1 y)"
        by (meson welltyped_is_ground)     

      moreover have "ρ1 (the_inv ρ1 (Var x)) = Var x"
        by (metis ‹Var x ∈ ρ1 ` clause.vars premise1› image_iff renaming(1) term_subst_is_renaming_iff the_inv_f_f)

      ultimately show ?thesis
        using True
        unfolding 𝒱3_def y_def
        by simp
    next
      case False
      then have "Var x ∈ ρ2 ` clause.vars premise2"
        using x_in_vars
        by (metis Un_iff image_eqI renaming(2) renaming_vars_clause)

      then have y_in_vars: "the_inv ρ2 (Var x) ∈ clause.vars premise2"
        by (metis (no_types, lifting) image_iff renaming(2) term_subst_is_renaming_iff the_inv_f_f)

      define y where "y ≡ the_inv ρ2 (Var x)"

      have "term.is_ground (Var y ⋅t ρ2 ⋅t γ)"
        using term_subst.is_ground_subst_is_ground typing(3) by blast

      moreover have "welltyped typeof_fun 𝒱2 (Var y ⋅t ρ2 ⋅t γ) (𝒱2 y)"
        using typing(5) y_in_vars
        unfolding welltypedσ_on_def y_def
        by (simp add: subst_compose)

      ultimately have "welltyped typeof_fun 𝒱3 (Var y ⋅t ρ2 ⋅t γ) (𝒱2 y)"
        by (meson welltyped_is_ground)     

      moreover have "ρ2 (the_inv ρ2 (Var x)) = Var x"
        by (metis ‹Var x ∈ ρ2 ` clause.vars premise2› image_iff renaming(2) 
            term_subst_is_renaming_iff the_inv_f_f)

      ultimately show ?thesis
        using False
        unfolding 𝒱3_def y_def
        by simp
    qed

    then show "welltyped typeof_fun 𝒱3 (γ x) (𝒱3 x)"
      unfolding γ_x.
  qed

  have "term1 ⋅t ρ1 ⋅t γ = term2 ⋅t ρ2 ⋅t γ"
    unfolding term1_γ term2_γ ..

  moreover have 
    "∃τ. welltyped typeof_fun 𝒱3 (term1 ⋅t ρ1) τ ∧ welltyped typeof_fun 𝒱3 (term2 ⋅t ρ2) τ"
  proof-
    have "welltypedc typeof_fun 𝒱2 (premise2 ⋅ ρ2 ⋅ γ)"
      using typing
      by (metis clause.subst_comp_subst welltypedσ_on_welltypedc)

    then obtain τ where 
      "welltyped typeof_fun 𝒱2 (term.from_ground termG1) τ" 
      unfolding premise2_γ ground_superpositionI 
      by clause_simp

    then have 
      "welltyped typeof_fun 𝒱3 (term.from_ground termG1) τ" 
      using welltyped_is_ground
      by (metis term.ground_is_ground)+

    then have 
      "welltyped typeof_fun 𝒱3 (term.from_ground termG1) τ"
      by auto

    then have 
        "welltyped typeof_fun 𝒱3 (term1 ⋅t ρ1 ⋅t γ) τ" "welltyped typeof_fun 𝒱3 (term2 ⋅t ρ2 ⋅t γ) τ"
      using term1_γ term2_γ
      by presburger+

    moreover have 
      "term.vars (term1 ⋅t ρ1) ⊆ clause.vars (premise1 ⋅ ρ1)"
      "term.vars (term2 ⋅t ρ2) ⊆ clause.vars (premise2 ⋅ ρ2)"
      unfolding premise1 literal1 subst_clause_add_mset term1_with_context premise2 literal2
      by clause_simp

    ultimately have 
        "welltyped typeof_fun 𝒱3 (term1 ⋅t ρ1) τ" "welltyped typeof_fun 𝒱3 (term2 ⋅t ρ2) τ"
      using wt_γ
      unfolding welltypedσ_on_def 
      by (meson sup_ge1 sup_ge2 welltypedσ_on_subset welltypedσ_on_term wt_γ)+

    then show ?thesis
      by blast
  qed

  ultimately obtain μ σ where μ: 
    "term_subst.is_imgu μ {{term1 ⋅t ρ1, term2 ⋅t ρ2}}" 
    "γ = μ ⊙ σ" 
    "welltyped_imgu' typeof_fun 𝒱3 (term1 ⋅t ρ1) (term2 ⋅t ρ2) μ"
    using welltyped_imgu'_exists
    by (smt (verit, del_insts))

  define conclusion' where 
    conclusion': "conclusion' ≡
      add_mset (?𝒫 (Upair term2'_with_context (term1' ⋅t ρ1))) (premise1' ⋅ ρ1 + premise2' ⋅ ρ2) ⋅ μ"

  show ?thesis
  proof(rule that)
    show "superposition (premise2, 𝒱2) (premise1, 𝒱1) (conclusion', 𝒱3)"
    proof(rule superpositionI)
      show "term_subst.is_renaming ρ1"
        using renaming(1).
    next
      show "term_subst.is_renaming ρ2"
        using renaming(2).
    next 
      show "premise1 = add_mset literal1 premise1'"
        using premise1.
    next
      show "premise2 = add_mset literal2 premise2'"
        using premise2.
    next
      show "?𝒫 ∈ {Pos, Neg}"
        by simp
    next
      show "literal1 = ?𝒫 (Upair context1⟨term1⟩ term1')"
        unfolding literal1 term1_with_context..
    next
      show "literal2 = term2 ≈ term2'"
        using literal2.
    next
      show "is_Fun term1"
        using term1_not_Var.
    next
      show "term_subst.is_imgu μ {{term1 ⋅t ρ1, term2 ⋅t ρ2}}"
        using μ(1).
    next
      note premises_clause_to_ground_inverse = assms(9, 10)[THEN clause.to_ground_inverse]  
      note premise_groundings = assms(10, 9)[unfolded μ(2) clause.subst_comp_subst]

      have "premise2 ⋅ ρ2 ⋅ μ ⋅ σ ≺c premise1 ⋅ ρ1 ⋅ μ ⋅ σ"
        using ground_superpositionI(3)
        unfolding premiseG1 premiseG2 lesscG_lessc premises_clause_to_ground_inverse 
        unfolding μ(2) clause.subst_comp_subst
        by blast

      then show "¬ premise1 ⋅ ρ1 ⋅ μ ≼c premise2 ⋅ ρ2 ⋅ μ"
        using lessc_less_eqc_ground_subst_stability[OF premise_groundings]
        by blast
    next
      show "?𝒫 = Pos 
              ∧ select premise1 = {#} 
              ∧ is_strictly_maximall (literal1 ⋅l ρ1 ⋅l μ) (premise1 ⋅ ρ1 ⋅ μ) 
          ∨ ?𝒫 = Neg 
              ∧ (select premise1 = {#} ∧ is_maximall (literal1 ⋅l ρ1 ⋅l μ) (premise1 ⋅ ρ1 ⋅ μ) 
                 ∨ is_maximall (literal1 ⋅l ρ1 ⋅l μ) ((select premise1) ⋅ ρ1 ⋅ μ))"
      proof(cases "?𝒫 = Pos")
        case True
        moreover then have select_empty: "select premise1 = {#}"
          using clause_subst_empty select(1) ground_superpositionI(9) 
          by clause_auto

        moreover have "is_strictly_maximall (literal1 ⋅l ρ1 ⋅l μ ⋅l σ) (premise1 ⋅ ρ1 ⋅ μ ⋅ σ)"
          using True pos_literalG1_is_strictly_maximall
          unfolding literal1_γ[symmetric] μ(2)
          by force

        moreover then have "is_strictly_maximall (literal1 ⋅l ρ1 ⋅l μ) (premise1 ⋅ ρ1 ⋅ μ)"
          using 
            is_strictly_maximall_ground_subst_stability'[OF
              _
              premise1_grounding[unfolded μ(2) clause.subst_comp_subst]
              ]
            clause.subst_in_to_set_subst
            literal1_in_premise1
          by blast

        ultimately show ?thesis
          by auto
      next
        case 𝒫_not_Pos: False
        then have 𝒫G_Neg: "𝒫G = Neg"
          using ground_superpositionI(4)
          by fastforce

        show ?thesis
        proof(cases ?selectG_empty)
          case selectG_empty: True

          then have "select premise1 = {#}"
            using clause_subst_empty select(1) ground_superpositionI(9) 𝒫G_Neg
            by clause_auto

          moreover have "is_maximall (literal1 ⋅l ρ1 ⋅l μ ⋅l σ) (premise1 ⋅ ρ1 ⋅ μ ⋅ σ)"
            using neg_literalG1_is_maximall[OF selectG_empty]
            unfolding literal1_γ[symmetric] μ(2)
            by simp

          moreover then have "is_maximall (literal1 ⋅l ρ1 ⋅l μ) (premise1 ⋅ ρ1 ⋅ μ)"
            using 
              is_maximall_ground_subst_stability'[OF 
                _  
                premise1_grounding[unfolded μ(2) clause.subst_comp_subst]
                ]
              clause.subst_in_to_set_subst
              literal1_in_premise1
            by blast

          ultimately show ?thesis
            using 𝒫G_Neg
            by simp
        next
          case selectG_not_empty: False

          have selected_grounding: "clause.is_ground (select premise1 ⋅ ρ1 ⋅ μ ⋅ σ)"
            using select_subst(1)[OF premise1_grounding] select(1)
            unfolding μ(2) clause.subst_comp_subst
            by (metis clause.ground_is_ground)

          note selected_subst =
            literal1_selected[
              OF 𝒫G_Neg selectG_not_empty, 
              THEN maximall_in_clause, 
              THEN clause.subst_in_to_set_subst] 

          have "is_maximall (literal1  ⋅l ρ1 ⋅l γ) (select premise1 ⋅ ρ1 ⋅ γ)"  
            using selectG_not_empty ground_superpositionI(9) 𝒫G_Neg 
            unfolding is_maximal_lit_iff_is_maximall literal1_γ[symmetric] select(1)
            by simp

          then have "is_maximall (literal1 ⋅l ρ1 ⋅l μ) ((select premise1) ⋅ ρ1 ⋅ μ)"
            using is_maximall_ground_subst_stability'[OF _ selected_grounding] selected_subst
            by (metis μ(2) clause.subst_comp_subst literal.subst_comp_subst)

          with selectG_not_empty 𝒫G_Neg show ?thesis
            by simp
        qed
      qed
    next
      show "select premise2 = {#}"
        using ground_superpositionI(10) select(2)
        by clause_auto
    next 
      have "is_strictly_maximall (literal2 ⋅l ρ2 ⋅l μ ⋅l σ) (premise2 ⋅ ρ2 ⋅ μ ⋅ σ)"
        using literalG2_is_strictly_maximall
        unfolding literal2_γ[symmetric] μ(2)
        by simp

      then show "is_strictly_maximall (literal2 ⋅l ρ2 ⋅l μ) (premise2 ⋅ ρ2 ⋅ μ)"
        using 
          is_strictly_maximall_ground_subst_stability'[OF 
            _  premise2_grounding[unfolded μ(2) clause.subst_comp_subst]]
          literal2_in_premise2
          clause.subst_in_to_set_subst
        by blast
    next
      have term_groundings: 
        "term.is_ground (term1' ⋅t ρ1 ⋅t μ ⋅t σ)" 
        "term.is_ground (context1⟨term1⟩ ⋅t ρ1 ⋅t μ ⋅t σ)" 
        unfolding 
          term1_with_context[symmetric]  
          term1_with_context_γ[unfolded μ(2) term_subst.subst_comp_subst]
          term1'_γ[unfolded μ(2) term_subst.subst_comp_subst]
        by simp_all

      have "term1' ⋅t ρ1 ⋅t μ ⋅t σ ≺t context1⟨term1⟩ ⋅t ρ1 ⋅t μ ⋅t σ"
        using ground_superpositionI(7) 
        unfolding 
          term1'_γ[unfolded μ(2) term_subst.subst_comp_subst]
          term1_with_context[symmetric]
          term1_with_context_γ[unfolded μ(2) term_subst.subst_comp_subst]
          lesstG_def
          ground_term_with_context(3).

      then show "¬ context1⟨term1⟩ ⋅t ρ1 ⋅t μ ≼t term1' ⋅t ρ1 ⋅t μ"
        using lesst_less_eqt_ground_subst_stability[OF term_groundings]
        by blast
    next
      have term_groundings: 
        "term.is_ground (term2' ⋅t ρ2 ⋅t μ ⋅t σ)"
        "term.is_ground (term2 ⋅t ρ2 ⋅t μ ⋅t σ)"
        unfolding
          term2_γ[unfolded μ(2) term_subst.subst_comp_subst]
          term2'_γ[unfolded μ(2) term_subst.subst_comp_subst]
        by simp_all

      have "term2' ⋅t ρ2 ⋅t μ ⋅t σ ≺t term2 ⋅t ρ2 ⋅t μ ⋅t σ"
        using ground_superpositionI(8)
        unfolding
          term2_γ[unfolded μ(2) term_subst.subst_comp_subst]       
          term2'_γ[unfolded μ(2) term_subst.subst_comp_subst]
          lesstG_def.

      then show "¬ term2 ⋅t ρ2 ⋅t μ ≼t term2' ⋅t ρ2 ⋅t μ"
        using lesst_less_eqt_ground_subst_stability[OF term_groundings]
        by blast
    next
      show 
        "conclusion' = add_mset (?𝒫 (Upair (context1 ⋅tc ρ1)⟨term2' ⋅t ρ2⟩ (term1' ⋅t ρ1))) 
          (premise1' ⋅ ρ1 + premise2' ⋅ ρ2) ⋅ μ"
        unfolding term2'_with_context conclusion'..
      show "welltyped_imgu' typeof_fun 𝒱3 (term1 ⋅t ρ1) (term2 ⋅t ρ2) μ"
        using μ(3) by blast

      show "clause.vars (premise1 ⋅ ρ1) ∩ clause.vars (premise2 ⋅ ρ2) = {}"
        using renaming(3). 

      show "∀x∈clause.vars (premise1 ⋅ ρ1). 𝒱1 (the_inv ρ1 (Var x)) = 𝒱3 x"
        unfolding 𝒱3_def
        by meson

      show "∀x∈clause.vars (premise2 ⋅ ρ2). 𝒱2 (the_inv ρ2 (Var x)) = 𝒱3 x"
        unfolding 𝒱3_def
        using renaming(3)
        by (meson disjoint_iff)

      show "welltypedσ_on (clause.vars premise1) typeof_fun 𝒱1 ρ1"
        using typing(6).

      show "welltypedσ_on (clause.vars premise2) typeof_fun 𝒱2 ρ2"
        using typing(7).

      have "∃τ. welltyped typeof_fun 𝒱2 term2 τ ∧ welltyped typeof_fun 𝒱2 term2' τ"
        using typing(2)
        unfolding premise2 literal2 welltypedc_def welltypedl_def welltypeda_def
        by auto

      then show "⋀τ τ'. ⟦has_type typeof_fun 𝒱2 term2 τ; has_type typeof_fun 𝒱2 term2' τ'⟧ ⟹ τ = τ'"
        by (metis welltyped_right_unique has_type_welltyped right_uniqueD) 

      show "all_types 𝒱1" "all_types 𝒱2"
        using typing
        by auto
    qed

    have "term_subst.is_idem μ"
      using μ(1)
      by (simp add: term_subst.is_imgu_iff_is_idem_and_is_mgu)  

    then have μ_γ: "μ ⊙ γ = γ"
      unfolding μ(2) term_subst.is_idem_def
      by (metis subst_compose_assoc)

    have conclusion'_γ: "conclusion' ⋅ γ = conclusion ⋅ γ"
    proof-
      have "conclusion ⋅ γ = 
              add_mset (?𝒫 (Upair (context.from_ground contextG)⟨term.from_ground termG3⟩ (term.from_ground termG2))) 
                (clause.from_ground premiseG1' + clause.from_ground premiseG2')"
      proof-
        have "⟦
          conclusionG = add_mset (contextG⟨termG3⟩G ≈ termG2) (premiseG1' + premiseG2');
          clause.from_ground (clause.to_ground (conclusion ⋅ γ)) = conclusion ⋅ γ; 𝒫G = Pos⟧
          ⟹ conclusion ⋅ γ =
              add_mset
               ((if Pos = Pos then Pos else Neg)
                 (Upair (term.from_ground contextG⟨termG3⟩G) (term.from_ground termG2)))
               (clause.from_ground premiseG1' + clause.from_ground premiseG2')"
          by (simp add: literal_from_ground_atom_from_ground(2) clause_from_ground_add_mset 
              atom_from_ground_term_from_ground)

        moreover have "⟦
          conclusionG = add_mset (contextG⟨termG3⟩G !≈ termG2) (premiseG1' + premiseG2');
          clause.from_ground (clause.to_ground (conclusion ⋅ γ)) = conclusion ⋅ γ; 𝒫G = Neg⟧
          ⟹ conclusion ⋅ γ =
              add_mset
               ((if Neg = Pos then Pos else Neg)
                 (Upair (term.from_ground contextG⟨termG3⟩G) (term.from_ground termG2)))
               (clause.from_ground premiseG1' + clause.from_ground premiseG2')"
          by (simp add: literal_from_ground_atom_from_ground(1) clause_from_ground_add_mset 
              atom_from_ground_term_from_ground)

        ultimately show ?thesis
          using ground_superpositionI(4, 12) clause.to_ground_inverse[OF conclusion_grounding] 
          unfolding ground_term_with_context(3) 
          by clause_simp
      qed
      
      then show ?thesis
        unfolding 
          conclusion'
          term2'_with_context_γ[symmetric]
          premise1'_γ[symmetric] 
          premise2'_γ[symmetric] 
          term1'_γ[symmetric]
          subst_clause_plus[symmetric] 
          subst_apply_term_ctxt_apply_distrib[symmetric]
          subst_atom[symmetric]
        unfolding
          clause.subst_comp_subst[symmetric]
          μ_γ
        by(simp add: subst_clause_add_mset subst_literal)
    qed

    have vars_conclusion': 
      "clause.vars conclusion' ⊆ clause.vars (premise1 ⋅ ρ1) ∪ clause.vars (premise2 ⋅ ρ2)"
    proof
      fix x 
      assume "x ∈ clause.vars conclusion'"

      then consider 
          (term2'_with_context) "x ∈ term.vars (term2'_with_context ⋅t μ)" 
        | (term1')  "x ∈ term.vars (term1' ⋅t ρ1 ⋅t μ)"  
        | (premise1')  "x ∈ clause.vars (premise1' ⋅ ρ1 ⋅ μ)"  
        | (premise2')  "x ∈ clause.vars (premise2' ⋅ ρ2 ⋅ μ)"  
        unfolding conclusion' subst_clause_add_mset subst_clause_plus subst_literal
        by clause_simp
  
      then show "x ∈ clause.vars (premise1 ⋅ ρ1) ∪ clause.vars (premise2 ⋅ ρ2)"
      proof(cases)
        case t: term2'_with_context
        then show ?thesis 
          using vars_context_imgu[OF μ(1)]  vars_term_imgu[OF μ(1)]
          unfolding premise1 literal1 term1_with_context premise2 literal2 term2'_with_context
          apply clause_simp
          by blast
      next
        case term1'
        then show ?thesis
          using vars_term_imgu[OF μ(1)]
          unfolding premise1 subst_clause_add_mset literal1 term1_with_context premise2 literal2
          by clause_simp
      next
        case premise1'
        then show ?thesis 
          using vars_clause_imgu[OF μ(1)]
          unfolding premise1 subst_clause_add_mset literal1 term1_with_context premise2 literal2
          by clause_simp
       next
        case premise2'
        then show ?thesis 
          using vars_clause_imgu[OF μ(1)]
          unfolding premise1 subst_clause_add_mset literal1 term1_with_context premise2 literal2
          by clause_simp
      qed
    qed

    have surjx: "surj (λx. the_inv ρ2 (Var x))"
      using surj_the_inv[OF renaming(2)].

    have yy: 
      "⋀P Q b ty. {x. (if b x then P x else Q x) = ty } = 
        {x. b x ∧ P x = ty} ∪ {x. ¬b x ∧ Q x = ty}"
      by auto

    have qq: "⋀ty. infinite {x. 𝒱2 (the_inv ρ2 (Var x)) = ty}"
      using needed[OF surjx typing(9)[unfolded all_types_def, rule_format]].

    have zz: 
      "⋀ty. {x. x ∉ clause.vars (premise1 ⋅ ρ1) ∧ 𝒱2 (the_inv ρ2 (Var x)) = ty} = 
            {x. 𝒱2 (the_inv ρ2 (Var x)) = ty} - {x. x ∈ clause.vars (premise1 ⋅ ρ1)}"
      by auto

    have "⋀ty. infinite {x. x ∉ clause.vars (premise1 ⋅ ρ1) ∧ 𝒱2 (the_inv ρ2 (Var x)) = ty}"
      unfolding zz
      using qq
      by auto

    then have all_types_𝒱3: "all_types 𝒱3"   
      unfolding 𝒱3_def all_types_def  yy     
      by auto

    show "ιG ∈ inference_groundings (Infer [(premise2, 𝒱2), (premise1, 𝒱1)] (conclusion', 𝒱3))"
    proof-
      have " ⟦conclusion' ⋅ γ = conclusion ⋅ γ;
         ground.ground_superposition (clause.to_ground (premise2 ⋅ ρ2 ⋅ γ))
          (clause.to_ground (premise1 ⋅ ρ1 ⋅ γ)) (clause.to_ground (conclusion ⋅ γ));
         welltypedσ_on (clause.vars conclusion') typeof_fun 𝒱3 γ; all_types 𝒱3⟧
        ⟹ First_Order_Type_System.welltypedc typeof_fun 𝒱3 conclusion'"
        using ‹superposition (premise2, 𝒱2) (premise1, 𝒱1) (conclusion', 𝒱3)› 
          superposition_preserves_typing typing(1) typing(2) by blast

      then have 
        "is_inference_grounding (Infer [(premise2, 𝒱2), (premise1, 𝒱1)] (conclusion', 𝒱3)) ιG γ ρ1 ρ2"
        using 
          conclusion'_γ ground_superposition 
          welltypedσ_on_subset[OF  wt_γ vars_conclusion'] 
          all_types_𝒱3
        unfolding is_inference_grounding_def
        unfolding ground.G_Inf_def ιG
        by(auto simp: typing renaming premise1_grounding premise2_grounding conclusion_grounding)

      then show ?thesis
        using is_inference_grounding_inference_groundings
        by blast
    qed

    show "conclusion' ⋅ γ = conclusion ⋅ γ"
      using conclusion'_γ.
  qed
qed  

lemma eq_resolution_ground_instance: 
  assumes 
    "ιG ∈ ground.eq_resolution_inferences"
    "ιG ∈ ground.Inf_from_q selectG (⋃(clause_groundings typeof_fun ` premises))"
    "subst_stability_on typeof_fun premises"
  obtains ι where 
    "ι ∈ Inf_from premises" 
    "ιG ∈ inference_groundings ι"
proof-
  obtain premiseG conclusionG where 
    ιG : "ιG = Infer [premiseG] conclusionG" and
    ground_eq_resolution: "ground.ground_eq_resolution premiseG conclusionG"
    using assms(1)
    by blast

  have premiseG_in_groundings: "premiseG ∈ ⋃(clause_groundings typeof_fun ` premises)"
    using assms(2)
    unfolding ιG ground.Inf_from_q_def ground.Inf_from_def
    by simp

  obtain premise "conclusion" γ 𝒱 where
    "clause.from_ground premiseG = premise ⋅ γ" and
    "clause.from_ground conclusionG = conclusion ⋅ γ" and
    select: "clause.from_ground (selectG premiseG) = select premise ⋅ γ" and
    premise_in_premises: "(premise, 𝒱) ∈ premises" and
    typing: "welltypedc typeof_fun 𝒱 premise"
    "term_subst.is_ground_subst γ"
    "welltypedσ_on (clause.vars premise) typeof_fun 𝒱 γ"
    "all_types 𝒱"
  proof-
    have x: "⋀a b. ⟦⋀premise γ conclusion 𝒱.
               ⟦clause.from_ground premiseG = premise ⋅ γ;
                clause.from_ground conclusionG = conclusion ⋅ γ;
                clause.from_ground (selectG premiseG) = select premise ⋅ γ; 
                (premise, 𝒱) ∈ premises;
                First_Order_Type_System.welltypedc typeof_fun 𝒱 premise; 
                term_subst.is_ground_subst γ;
                welltypedσ_on (clause.vars premise) typeof_fun 𝒱 γ; all_types 𝒱⟧
               ⟹ thesis;
            ∀y∈premises.
               ∀premiseG∈clause_groundings typeof_fun y.
                  ∃x∈premises.
                     case x of
                     (premise, 𝒱) ⇒
                       ∃γ. premise ⋅ γ = clause.from_ground premiseG ∧
                           selectG (clause.to_ground (premise ⋅ γ)) =
                           clause.to_ground (select premise ⋅ γ) ∧
                           First_Order_Type_System.welltypedc typeof_fun 𝒱 premise ∧
                           welltypedσ_on (clause.vars premise) typeof_fun 𝒱 γ ∧
                           term_subst.is_ground_subst γ ∧ all_types 𝒱;
            Infer [premiseG] conclusionG ∈ ground.G_Inf; (a, b) ∈ premises;
            premiseG ∈ clause_groundings typeof_fun (a, b)⟧
           ⟹ thesis"
      by (smt (verit, del_insts) case_prodE clause.ground_is_ground select_subst1 
          clause.subst_ident_if_ground clause.from_ground_inverse clause.to_ground_inverse)

    then show ?thesis
      using assms(2, 3) premiseG_in_groundings that
      unfolding ιG ground.Inf_from_q_def ground.Inf_from_def
      by auto
  qed

  then have
    premise_grounding: "clause.is_ground (premise ⋅ γ)" and
    premiseG: "premiseG = clause.to_ground (premise ⋅ γ)" and
    conclusion_grounding: "clause.is_ground (conclusion ⋅ γ)" and
    conclusionG: "conclusionG = clause.to_ground (conclusion ⋅ γ)"
    using clause.ground_is_ground clause.from_ground_inverse
    by(smt(verit))+

  obtain conclusion' where
    eq_resolution: "eq_resolution (premise, 𝒱) (conclusion', 𝒱)" and
    ιG: "ιG = Infer [clause.to_ground (premise ⋅ γ)] (clause.to_ground (conclusion' ⋅ γ))" and
    inference_groundings: "ιG ∈ inference_groundings (Infer [(premise, 𝒱)] (conclusion', 𝒱))" and  
    conclusion'_conclusion: "conclusion' ⋅ γ = conclusion ⋅ γ"
    using
      eq_resolution_lifting[OF 
        premise_grounding 
        conclusion_grounding 
        select[unfolded premiseG] 
        ground_eq_resolution[unfolded premiseG conclusionG]
        typing
        ]
    unfolding premiseG conclusionG ιG
    by metis

  let ?ι = "Infer [(premise, 𝒱)] (conclusion', 𝒱)"

  show ?thesis
  proof(rule that)
    show "?ι ∈ Inf_from premises"
      using premise_in_premises eq_resolution
      unfolding Inf_from_def inferences_def inference_system.Inf_from_def
      by auto

    show "ιG ∈ inference_groundings ?ι"
      using inference_groundings.
  qed
qed 

lemma eq_factoring_ground_instance: 
  assumes 
    "ιG ∈ ground.eq_factoring_inferences"
    "ιG ∈ ground.Inf_from_q selectG (⋃(clause_groundings typeof_fun ` premises))"
    "subst_stability_on typeof_fun premises"
  obtains ι where 
    "ι ∈ Inf_from premises" 
    "ιG ∈ inference_groundings ι"
proof-
  obtain premiseG conclusionG where 
    ιG : "ιG = Infer [premiseG] conclusionG" and
    ground_eq_factoring: "ground.ground_eq_factoring premiseG conclusionG"
    using assms(1)
    by blast

  have premiseG_in_groundings: "premiseG ∈ ⋃(clause_groundings typeof_fun ` premises)"
    using assms(2)
    unfolding ιG ground.Inf_from_q_def ground.Inf_from_def
    by simp

  obtain premise "conclusion" γ 𝒱 where
    "clause.from_ground premiseG = premise ⋅ γ" and
    "clause.from_ground conclusionG = conclusion ⋅ γ" and
    select: "clause.from_ground (selectG (clause.to_ground (premise ⋅ γ))) = select premise ⋅ γ" and
    premise_in_premises: "(premise, 𝒱) ∈ premises" and
    typing:
    "welltypedc typeof_fun 𝒱 premise"
    "term_subst.is_ground_subst γ"
    "welltypedσ_on (clause.vars premise) typeof_fun 𝒱 γ"
    "all_types 𝒱"
    using assms(2, 3) premiseG_in_groundings
    unfolding ιG ground.Inf_from_q_def ground.Inf_from_def
    by (smt (verit) clause.subst_ident_if_ground clause.ground_is_ground 
        old.prod.case old.prod.exhaust select_subst1 clause.to_ground_inverse)

  then have 
    premise_grounding: "clause.is_ground (premise ⋅ γ)" and 
    premiseG: "premiseG = clause.to_ground (premise ⋅ γ)" and 
    conclusion_grounding: "clause.is_ground (conclusion ⋅ γ)" and
    conclusionG: "conclusionG = clause.to_ground (conclusion ⋅ γ)"
    by (smt(verit) clause.ground_is_ground clause.from_ground_inverse)+

  obtain conclusion' where 
    eq_factoring: "eq_factoring (premise, 𝒱) (conclusion', 𝒱)" and
    inference_groundings: "ιG ∈ inference_groundings (Infer [(premise, 𝒱)] (conclusion', 𝒱))" and  
    conclusion'_conclusion: "conclusion' ⋅ γ = conclusion ⋅ γ"
    using 
      eq_factoring_lifting[OF 
        premise_grounding 
        conclusion_grounding 
        select 
        ground_eq_factoring[unfolded premiseG conclusionG]
        ]
      typing
    unfolding premiseG conclusionG ιG
    by metis

  let ?ι = "Infer [(premise, 𝒱)] (conclusion', 𝒱)"

  show ?thesis
  proof(rule that)
    show "?ι ∈ Inf_from premises"
      using premise_in_premises eq_factoring
      unfolding Inf_from_def inferences_def inference_system.Inf_from_def
      by auto

    show "ιG ∈ inference_groundings ?ι"
      using inference_groundings.
  qed
qed

lemma subst_compose_if: "σ ⊙ (λvar. if var ∈ range_vars' σ then σ1 var else σ2 var) = σ ⊙ σ1"
  unfolding subst_compose_def range_vars'_def
  using term_subst_eq_conv
  by fastforce

lemma subst_compose_if': 
  assumes "range_vars' σ ∩ range_vars' σ' = {}"
  shows "σ ⊙ (λvar. if var ∈ range_vars' σ' then σ1 var else σ2 var) = σ ⊙ σ2"
proof-
  have "⋀x. σ x ⋅t (λvar. if var ∈ range_vars' σ' then σ1 var else σ2 var) = σ x ⋅t σ2"
  proof-
    fix x
    have "⋀xa. ⟦σ x = Var xa; xa ∈ range_vars' σ'⟧ ⟹ σ1 xa = σ2 xa"
      by (metis IntI assms emptyE subst_compose_def term.set_intros(3) 
          term_subst.comp_subst.left.right_neutral vars_term_range_vars')
    moreover have "⋀x1a x2 xa.
       ⟦σ x = Fun x1a x2; xa ∈ set x2⟧
       ⟹ xa ⋅t (λvar. if var ∈ range_vars' σ' then σ1 var else σ2 var) = xa ⋅t σ2"
      by (smt (verit, ccfv_threshold) UNIV_I UN_iff assms disjoint_iff image_iff range_vars'_def 
          term.set_intros(4) term_subst_eq_conv)

    ultimately show "σ x ⋅t (λvar. if var ∈ range_vars' σ' then σ1 var else σ2 var) = σ x ⋅t σ2"
      by(induction "σ x") auto
  qed

  then show ?thesis
    unfolding subst_compose_def    
    by presburger
qed

lemma is_ground_subst_if:
  assumes "term_subst.is_ground_subst γ1" "term_subst.is_ground_subst γ2"
  shows "term_subst.is_ground_subst (λvar. if b var then γ1 var else γ2 var)"
  using assms
  unfolding term_subst.is_ground_subst_def
  by (simp add: is_ground_iff)

lemma superposition_ground_instance: 
  assumes 
    "ιG ∈ ground.superposition_inferences"
    "ιG ∈ ground.Inf_from_q selectG (⋃ (clause_groundings typeof_fun ` premises))" 
    "ιG ∉ ground.GRed_I (⋃ (clause_groundings typeof_fun ` premises))"
    "subst_stability_on typeof_fun premises"
  obtains ι where 
    "ι ∈ Inf_from premises" 
    "ιG ∈ inference_groundings ι"
proof-
  obtain premiseG1 premiseG2 conclusionG where 
    ιG : "ιG = Infer [premiseG2, premiseG1] conclusionG" and
    ground_superposition: "ground.ground_superposition premiseG2 premiseG1 conclusionG"
    using assms(1)
    by blast

  have 
    premiseG1_in_groundings: "premiseG1 ∈ ⋃ (clause_groundings typeof_fun ` premises)" and  
    premiseG2_in_groundings: "premiseG2 ∈ ⋃ (clause_groundings typeof_fun ` premises)"
    using assms(2)
    unfolding ιG ground.Inf_from_q_def ground.Inf_from_def
    by simp_all

  obtain premise1 𝒱1 premise2 𝒱2 γ1 γ2 where
    premise1_γ1: "premise1 ⋅ γ1 = clause.from_ground premiseG1" and
    premise2_γ2: "premise2 ⋅ γ2 = clause.from_ground premiseG2" and
    select: 
    "clause.from_ground (selectG (clause.to_ground (premise1 ⋅ γ1))) = select premise1 ⋅ γ1"
    "clause.from_ground (selectG (clause.to_ground (premise2 ⋅ γ2))) = select premise2 ⋅ γ2" and
    premise1_in_premises: "(premise1, 𝒱1) ∈ premises" and
    premise2_in_premises: "(premise2, 𝒱2) ∈ premises" and 
    wt: 
    "welltypedσ_on (clause.vars premise1) typeof_fun 𝒱1 γ1"
    "welltypedσ_on (clause.vars premise2) typeof_fun 𝒱2 γ2"
    "term_subst.is_ground_subst γ1"
    "term_subst.is_ground_subst γ2" 
    "welltypedc typeof_fun 𝒱1 premise1"
    "welltypedc typeof_fun 𝒱2 premise2"
    "all_types 𝒱1" 
    "all_types 𝒱2" 
    using assms(2, 4) premiseG1_in_groundings premiseG2_in_groundings
    unfolding ιG ground.Inf_from_q_def ground.Inf_from_def   
    by (smt (verit, ccfv_threshold) case_prod_conv clause.ground_is_ground select_subst1 
        surj_pair clause.to_ground_inverse)

  obtain ρ1 ρ2 :: "('f, 'v) subst" where
    renaming: 
    "term_subst.is_renaming ρ1" 
    "term_subst.is_renaming ρ2"
    "ρ1 ` (clause.vars premise1) ∩ ρ2 ` (clause.vars premise2) = {}" and
    wt_ρ: 
    "welltypedσ_on (clause.vars premise1) typeof_fun 𝒱1 ρ1"
    "welltypedσ_on (clause.vars premise2) typeof_fun 𝒱2 ρ2"
    using welltyped_on_renaming_exists'[OF _ _ wt(7,8)[unfolded all_types_def, rule_format]] 
    by (metis clause.finite_vars(1))

  have renaming_distinct: "clause.vars (premise1 ⋅ ρ1) ∩ clause.vars (premise2 ⋅ ρ2) = {}"
    using renaming(3)
    unfolding renaming(1,2)[THEN renaming_vars_clause, symmetric]
    by blast

  from renaming obtain ρ1_inv ρ2_inv where
    ρ1_inv: "ρ1 ⊙ ρ1_inv = Var" and
    ρ2_inv: "ρ2 ⊙ ρ2_inv = Var"
    unfolding term_subst.is_renaming_def
    by blast

  have "select premise1 ⊆# premise1" "select premise2 ⊆# premise2"
    by (simp_all add: select_subset)

  then have select_subset: 
    "select premise1 ⋅ ρ1 ⊆# premise1 ⋅ ρ1" 
    "select premise2 ⋅ ρ2 ⊆# premise2 ⋅ ρ2"
    by (simp_all add: image_mset_subseteq_mono clause.subst_def)

  define γ where 
    γ: "⋀var. γ var ≡
          if var ∈ clause.vars (premise1 ⋅ ρ1)
          then (ρ1_inv ⊙ γ1) var 
          else (ρ2_inv ⊙ γ2) var"

  have γ1: "∀x∈ clause.vars premise1. (ρ1 ⊙ γ) x = γ1 x"
  proof(intro ballI)
    fix x
    assume x_in_vars: "x ∈ clause.vars premise1"

    obtain y where y: "ρ1 x = Var y"
      by (meson is_Var_def renaming(1) term_subst_is_renaming_iff)

    then have "y ∈ clause.vars (premise1 ⋅ ρ1)"
      using x_in_vars renaming(1) renaming_vars_clause by fastforce
    

    then have "γ y = ρ1_inv y ⋅t γ1"
      by (simp add: γ subst_compose)

    then show "(ρ1 ⊙ γ) x = γ1 x"
      by (metis y ρ1_inv eval_term.simps(1) subst_compose)
  qed

  have γ2: "∀x∈ clause.vars premise2. (ρ2 ⊙ γ) x = γ2 x"
  proof(intro ballI)
    fix x
    assume x_in_vars: "x ∈ clause.vars premise2"

    obtain y where y: "ρ2 x = Var y"
      by (meson is_Var_def renaming(2) term_subst_is_renaming_iff)

    then have "y ∈ clause.vars (premise2 ⋅ ρ2)"
      using x_in_vars renaming(2) renaming_vars_clause by fastforce
    

    then have "γ y = ρ2_inv y ⋅t γ2"
      using γ renaming_distinct subst_compose by fastforce

    then show "(ρ2 ⊙ γ) x = γ2 x"
      by (metis y ρ2_inv eval_term.simps(1) subst_compose)
  qed

  have γ1_is_ground: "∀x∈clause.vars premise1. term.is_ground (γ1 x)"
    by (metis Term.term.simps(17) insert_iff is_ground_iff term_subst.is_ground_subst_def wt(3))

  have γ2_is_ground: "∀x∈clause.vars premise2. term.is_ground (γ2 x)"
    by (metis Term.term.simps(17) insert_iff is_ground_iff term_subst.is_ground_subst_def wt(4))

  have wt_γ:
    "welltypedσ_on (clause.vars premise1) typeof_fun 𝒱1 (ρ1 ⊙ γ)"
    "welltypedσ_on (clause.vars premise2) typeof_fun 𝒱2 (ρ2 ⊙ γ)"
    using wt(1,2) welltypedσ_on_subset welltypedσ_welltypedσ_on γ1 γ2
    unfolding welltypedσ_on_def 
    by auto    

  have "term_subst.is_ground_subst (ρ1_inv ⊙ γ1)" "term_subst.is_ground_subst (ρ2_inv ⊙ γ2)"
    using term_subst.is_ground_subst_comp_right wt by blast+

  then have is_ground_subst_γ: "term_subst.is_ground_subst γ"
    unfolding γ
    using is_ground_subst_if
    by fast

  have premise1_γ: "premise1 ⋅ ρ1 ⋅ γ = clause.from_ground premiseG1" 
  proof -
    have "premise1 ⋅ ρ1 ⊙ (ρ1_inv ⊙ γ1) = clause.from_ground premiseG1"
      by (metis ρ1_inv premise1_γ1 subst_monoid_mult.mult.left_neutral subst_monoid_mult.mult_assoc)

    then show ?thesis
      using γ1 premise1_γ1 clause.subst_eq by fastforce
  qed

  have premise2_γ: "premise2 ⋅ ρ2 ⋅ γ = clause.from_ground premiseG2" 
  proof -
    have "premise2 ⋅ ρ2 ⊙ (ρ2_inv ⊙ γ2) = clause.from_ground premiseG2"
      by (metis ρ2_inv premise2_γ2 subst_monoid_mult.mult.left_neutral subst_monoid_mult.mult_assoc)

    then show ?thesis
      using γ2 premise2_γ2 clause.subst_eq by force
  qed

  have "premise1 ⋅ ρ1 ⋅ γ = premise1 ⋅ γ1"
    by (simp add: premise1_γ premise1_γ1)

  moreover have "select premise1 ⋅ ρ1 ⋅ γ = select premise1 ⋅ γ1"
  proof-
    have "clause.vars (select premise1 ⋅ ρ1) ⊆ clause.vars (premise1 ⋅ ρ1)"
      using select_subset(1) clause_submset_vars_clause_subset by blast

    then show ?thesis
      unfolding γ 
      by (smt (verit, best) ρ1_inv clause.subst_eq subsetD 
          clause.comp_subst.left.monoid_action_compatibility 
          term_subst.comp_subst.left.right_neutral)
  qed

  ultimately have select1: 
    "clause.from_ground (selectG (clause.to_ground (premise1 ⋅ ρ1 ⋅ γ))) = select premise1 ⋅ ρ1 ⋅ γ"
    using select(1)
    by argo
  
  have "premise2 ⋅ ρ2 ⋅ γ = premise2 ⋅ γ2"
    by (simp add: premise2_γ premise2_γ2)

  moreover have "select premise2 ⋅ ρ2 ⋅ γ = select premise2 ⋅ γ2"
   proof-
    have "clause.vars (select premise2 ⋅ ρ2) ⊆ clause.vars (premise2 ⋅ ρ2)"
      using select_subset(2) clause_submset_vars_clause_subset by blast

    then show ?thesis
      unfolding γ 
      by (smt (verit, best) γ2 γ ‹select premise2 ⊆# premise2› clause_submset_vars_clause_subset
          clause.subst_eq subset_iff clause.comp_subst.left.monoid_action_compatibility)
  qed

  ultimately have select2: 
    "clause.from_ground (selectG (clause.to_ground (premise2 ⋅ ρ2 ⋅ γ))) = select premise2 ⋅ ρ2 ⋅ γ"   
    using select(2) 
    by argo

  obtain "conclusion" where 
    conclusion_γ: "conclusion ⋅ γ = clause.from_ground conclusionG"
    by (meson clause.ground_is_ground clause.subst_ident_if_ground)

  then have 
    premise1_grounding: "clause.is_ground (premise1 ⋅ ρ1 ⋅ γ)" and 
    premise2_grounding: "clause.is_ground (premise2 ⋅ ρ2 ⋅ γ)" and 
    premiseG1: "premiseG1 = clause.to_ground (premise1 ⋅ ρ1 ⋅ γ)" and 
    premiseG2: "premiseG2 = clause.to_ground (premise2 ⋅ ρ2 ⋅ γ)" and 
    conclusion_grounding: "clause.is_ground (conclusion ⋅ γ)" and
    conclusionG: "conclusionG = clause.to_ground (conclusion ⋅ γ)"
    by (simp_all add: premise1_γ premise2_γ)

  have "clause_groundings typeof_fun (premise1, 𝒱1) ∪ clause_groundings typeof_fun (premise2, 𝒱2)
     ⊆ ⋃ (clause_groundings typeof_fun ` premises)"
    using premise1_in_premises premise2_in_premises by blast

  then have ιG_not_redunant:
    "ιG ∉ ground.GRed_I (clause_groundings typeof_fun (premise1, 𝒱1) ∪ clause_groundings typeof_fun (premise2, 𝒱2))"
    using assms(3) ground.Red_I_of_subset
    by blast

  then obtain conclusion' 𝒱3 where 
    superposition: "superposition (premise2, 𝒱2) (premise1, 𝒱1) (conclusion', 𝒱3)" and
    inference_groundings: 
      "ιG ∈ inference_groundings (Infer [(premise2, 𝒱2), (premise1, 𝒱1)] (conclusion', 𝒱3))" and  
    conclusion'_γ_conclusion_γ: "conclusion' ⋅ γ = conclusion ⋅ γ"
    using 
      superposition_lifting[OF 
        renaming(1,2)
        renaming_distinct
        premise1_grounding 
        premise2_grounding 
        conclusion_grounding
        select1
        select2
        ground_superposition[unfolded  premiseG2 premiseG1 conclusionG]
        ιG_not_redunant[unfolded ιG premiseG2 premiseG1 conclusionG]
        wt(5, 6)
        is_ground_subst_γ
        wt_γ
        wt_ρ
        wt(7, 8)
        ]
    unfolding ιG conclusionG premiseG1 premiseG2 
    by blast

  let ?ι = "Infer [(premise2, 𝒱2), (premise1, 𝒱1)] (conclusion', 𝒱3)"

  show ?thesis
  proof(rule that)
    show "?ι ∈ Inf_from premises"
      using premise1_in_premises premise2_in_premises superposition
      unfolding Inf_from_def inferences_def inference_system.Inf_from_def
      by auto

    show "ιG ∈ inference_groundings ?ι"
      using inference_groundings.
  qed
qed

lemma ground_instances: 
  assumes 
    "ιG ∈ ground.Inf_from_q selectG (⋃ (clause_groundings typeof_fun ` premises))" 
    "ιG ∉ ground.Red_I (⋃ (clause_groundings typeof_fun ` premises))"
    "subst_stability_on typeof_fun premises"
  obtains ι where 
    "ι ∈ Inf_from premises" 
    "ιG ∈ inference_groundings ι"
proof-
  have "ιG ∈ ground.superposition_inferences ∨
        ιG ∈ ground.eq_resolution_inferences ∨
        ιG ∈ ground.eq_factoring_inferences"
    using assms(1)
    unfolding 
      ground.Inf_from_q_def 
      ground.Inf_from_def 
      ground.G_Inf_def 
      inference_system.Inf_from_def
    by fastforce

  then show ?thesis
  proof(elim disjE)
    assume "ιG ∈ ground.superposition_inferences"
    then show ?thesis
      using that superposition_ground_instance assms
      by blast
  next
    assume "ιG ∈ ground.eq_resolution_inferences"  
    then show ?thesis
      using that eq_resolution_ground_instance assms
      by blast
  next
    assume "ιG ∈ ground.eq_factoring_inferences"
    then show ?thesis
      using that eq_factoring_ground_instance assms
      by blast
  qed
qed

end

context first_order_superposition_calculus
begin

lemma overapproximation:
  obtains selectG where
    "ground_Inf_overapproximated selectG premises"
    "is_grounding selectG"
proof-
  obtain selectG where   
    subst_stability: "select_subst_stability_on typeof_fun select selectG premises" and
    "is_grounding selectG" 
    using obtain_subst_stable_on_select_grounding
    by blast

  then interpret grounded_first_order_superposition_calculus
    where selectG = selectG
    by unfold_locales

  have overapproximation: "ground_Inf_overapproximated selectG premises"
    using ground_instances[OF _ _ subst_stability]
    by auto

  show thesis
    using that[OF overapproximation selectG].
qed

sublocale statically_complete_calculus "⊥F" inferences entails_𝒢 Red_I_𝒢 Red_F_𝒢
proof(unfold static_empty_ord_inter_equiv_static_inter, 
    rule stat_ref_comp_to_non_ground_fam_inter, 
    rule ballI)
  fix selectG
  assume "selectG ∈ selectGs"
  then interpret grounded_first_order_superposition_calculus
    where selectG = selectG
    by unfold_locales (simp add: selectGs_def)

  show "statically_complete_calculus
          ground.G_Bot
          ground.G_Inf
          ground.G_entails
          ground.Red_I
          ground.Red_F"
    using ground.statically_complete_calculus_axioms.
next
  fix clauses

  have "⋀clauses. ∃selectG ∈ selectGs. ground_Inf_overapproximated selectG clauses" 
    using overapproximation
    unfolding selectGs_def
    by (smt (verit, best) mem_Collect_eq)

  then show "empty_ord.saturated clauses ⟹ 
    ∃selectG ∈ selectGs. ground_Inf_overapproximated selectG clauses".
qed

end

end