exact ⟨ihp hb (hf.of_subset (fun x hx => Or.inl hx)), ihq hb (hf.of_subset (fun x hx => Or.inr hx))⟩
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ q✝ : Semiformula L ξ₁ n✝
ihp :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂},
    (∀ (x : Fin n✝), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom p✝ = ω₂.hom p✝
ihq :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂},
    (∀ (x : Fin n✝), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ q✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom q✝ = ω₂.hom q✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => x ∈ p✝.fvarList ∨ x ∈ q✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ ω₁.hom p✝ = ω₂.hom p✝ ∧ ω₁.hom q✝ = ω₂.hom q✝
no goals