Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁✝ : Type u_2
ξ₂✝ : Type u_3
ξ₃ : Type u_4
n n₁✝ n₂✝¹ n₂✝ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁✝ n₁✝ ξ₂✝ n₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
p : Semiformula L ξ₁ n₁
f g : ξ₁ → Semiterm L ξ₂ n₂
h : Function.funEqOn (fun x => x ∈ p.fv) f g
⊢ (rewriteMap f).hom p = (rewriteMap g).hom p
Tactic:
induction p using rec'
Proof state after:
case hverum
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁✝ : Type u_2
ξ₂✝ : Type u_3
ξ₃ : Type u_4
n n₁✝ n₂✝¹ n₂✝ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁✝ n₁✝ ξ₂✝ n₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
h : Function.funEqOn (fun x => x ∈ ⊤.fv) f g
⊢ (rewriteMap f).hom ⊤ = (rewriteMap g).hom ⊤

case hfalsum
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁✝ : Type u_2
ξ₂✝ : Type u_3
ξ₃ : Type u_4
n n₁✝ n₂✝¹ n₂✝ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁✝ n₁✝ ξ₂✝ n₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
h : Function.funEqOn (fun x => x ∈ ⊥.fv) f g
⊢ (rewriteMap f).hom ⊥ = (rewriteMap g).hom ⊥

case hrel
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁✝ : Type u_2
ξ₂✝ : Type u_3
ξ₃ : Type u_4
n n₁✝ n₂✝¹ n₂✝ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁✝ n₁✝ ξ₂✝ n₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r✝ v✝).fv) f g
⊢ (rewriteMap f).hom (rel r✝ v✝) = (rewriteMap g).hom (rel r✝ v✝)

case hnrel
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁✝ : Type u_2
ξ₂✝ : Type u_3
ξ₃ : Type u_4
n n₁✝ n₂✝¹ n₂✝ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁✝ n₁✝ ξ₂✝ n₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r✝ v✝).fv) f g
⊢ (rewriteMap f).hom (nrel r✝ v✝) = (rewriteMap g).hom (nrel r✝ v✝)

case hand
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁✝ : Type u_2
ξ₂✝ : Type u_3
ξ₃ : Type u_4
n n₁✝ n₂✝¹ n₂✝ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁✝ n₁✝ ξ₂✝ n₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p✝ q✝ : Semiformula L ξ₁ n✝
a✝¹ : Function.funEqOn (fun x => x ∈ p✝.fv) f g → (rewriteMap f).hom p✝ = (rewriteMap g).hom p✝
a✝ : Function.funEqOn (fun x => x ∈ q✝.fv) f g → (rewriteMap f).hom q✝ = (rewriteMap g).hom q✝
h : Function.funEqOn (fun x => x ∈ (p✝ ⋏ q✝).fv) f g
⊢ (rewriteMap f).hom (p✝ ⋏ q✝) = (rewriteMap g).hom (p✝ ⋏ q✝)

case hor
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁✝ : Type u_2
ξ₂✝ : Type u_3
ξ₃ : Type u_4
n n₁✝ n₂✝¹ n₂✝ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁✝ n₁✝ ξ₂✝ n₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p✝ q✝ : Semiformula L ξ₁ n✝
a✝¹ : Function.funEqOn (fun x => x ∈ p✝.fv) f g → (rewriteMap f).hom p✝ = (rewriteMap g).hom p✝
a✝ : Function.funEqOn (fun x => x ∈ q✝.fv) f g → (rewriteMap f).hom q✝ = (rewriteMap g).hom q✝
h : Function.funEqOn (fun x => x ∈ (p✝ ⋎ q✝).fv) f g
⊢ (rewriteMap f).hom (p✝ ⋎ q✝) = (rewriteMap g).hom (p✝ ⋎ q✝)

case hall
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁✝ : Type u_2
ξ₂✝ : Type u_3
ξ₃ : Type u_4
n n₁✝ n₂✝¹ n₂✝ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁✝ n₁✝ ξ₂✝ n₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
a✝ : Function.funEqOn (fun x => x ∈ p✝.fv) f g → (rewriteMap f).hom p✝ = (rewriteMap g).hom p✝
h : Function.funEqOn (fun x => x ∈ (∀' p✝).fv) f g
⊢ (rewriteMap f).hom (∀' p✝) = (rewriteMap g).hom (∀' p✝)

case hex
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁✝ : Type u_2
ξ₂✝ : Type u_3
ξ₃ : Type u_4
n n₁✝ n₂✝¹ n₂✝ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁✝ n₁✝ ξ₂✝ n₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
a✝ : Function.funEqOn (fun x => x ∈ p✝.fv) f g → (rewriteMap f).hom p✝ = (rewriteMap g).hom p✝
h : Function.funEqOn (fun x => x ∈ (∃' p✝).fv) f g
⊢ (rewriteMap f).hom (∃' p✝) = (rewriteMap g).hom (∃' p✝)