L : Language
L' : Language
M : Type w
N : Type ?u.124912
P : Type ?u.124915
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝ : Fin l → M
φ : BoundedFormula L α n✝
tf : α → Term L β
v : β → M
xs : Fin n✝ → M
n : ℕ
t : Term L (α ⊕ Fin n)
x : Fin n → M
⊢ realize (fun a => realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) a)) t =
    realize (Sum.elim (fun a => realize v (tf a)) x) t
L : Language
L' : Language
M : Type w
N : Type ?u.124912
P : Type ?u.124915
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝ : Fin l → M
φ : BoundedFormula L α n✝
tf : α → Term L β
v : β → M
xs : Fin n✝ → M
n : ℕ
t : Term L (α ⊕ Fin n)
x : Fin n → M
⊢ realize (Sum.elim v x) (Term.subst t (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr))) =
    realize (Sum.elim (fun a => realize v (tf a)) x) t
rw [Term.realize_subst]
case e_v.h
L : Language
L' : Language
M : Type w
N : Type ?u.124912
P : Type ?u.124915
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝ : Fin l → M
φ : BoundedFormula L α n✝
tf : α → Term L β
v : β → M
xs : Fin n✝ → M
n : ℕ
t : Term L (α ⊕ Fin n)
x : Fin n → M
a : α ⊕ Fin n
⊢ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) a) =
    Sum.elim (fun a => realize v (tf a)) x a
L : Language
L' : Language
M : Type w
N : Type ?u.124912
P : Type ?u.124915
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝ : Fin l → M
φ : BoundedFormula L α n✝
tf : α → Term L β
v : β → M
xs : Fin n✝ → M
n : ℕ
t : Term L (α ⊕ Fin n)
x : Fin n → M
⊢ realize (fun a => realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) a)) t =
    realize (Sum.elim (fun a => realize v (tf a)) x) t
rcongr a
case e_v.h.inl
L : Language
L' : Language
M : Type w
N : Type ?u.124912
P : Type ?u.124915
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝ : Fin l → M
φ : BoundedFormula L α n✝
tf : α → Term L β
v : β → M
xs : Fin n✝ → M
n : ℕ
t : Term L (α ⊕ Fin n)
x : Fin n → M
val✝ : α
⊢ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) (Sum.inl val✝)) =
    Sum.elim (fun a => realize v (tf a)) x (Sum.inl val✝)

case e_v.h.inr
L : Language
L' : Language
M : Type w
N : Type ?u.124912
P : Type ?u.124915
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝ : Fin l → M
φ : BoundedFormula L α n✝
tf : α → Term L β
v : β → M
xs : Fin n✝ → M
n : ℕ
t : Term L (α ⊕ Fin n)
x : Fin n → M
val✝ : Fin n
⊢ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) (Sum.inr val✝)) =
    Sum.elim (fun a => realize v (tf a)) x (Sum.inr val✝)
case e_v.h
L : Language
L' : Language
M : Type w
N : Type ?u.124912
P : Type ?u.124915
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝ : Fin l → M
φ : BoundedFormula L α n✝
tf : α → Term L β
v : β → M
xs : Fin n✝ → M
n : ℕ
t : Term L (α ⊕ Fin n)
x : Fin n → M
a : α ⊕ Fin n
⊢ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) a) =
    Sum.elim (fun a => realize v (tf a)) x a
cases a
no goals
case e_v.h.inl
L : Language
L' : Language
M : Type w
N : Type ?u.124912
P : Type ?u.124915
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝ : Fin l → M
φ : BoundedFormula L α n✝
tf : α → Term L β
v : β → M
xs : Fin n✝ → M
n : ℕ
t : Term L (α ⊕ Fin n)
x : Fin n → M
val✝ : α
⊢ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) (Sum.inl val✝)) =
    Sum.elim (fun a => realize v (tf a)) x (Sum.inl val✝)
simp only [Sum.elim_inl, Function.comp_apply, Term.realize_relabel, Sum.elim_comp_inl]
no goals
case e_v.h.inr
L : Language
L' : Language
M : Type w
N : Type ?u.124912
P : Type ?u.124915
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝ : Fin l → M
φ : BoundedFormula L α n✝
tf : α → Term L β
v : β → M
xs : Fin n✝ → M
n : ℕ
t : Term L (α ⊕ Fin n)
x : Fin n → M
val✝ : Fin n
⊢ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) (Sum.inr val✝)) =
    Sum.elim (fun a => realize v (tf a)) x (Sum.inr val✝)
rfl
no goals
L : Language
L' : Language
M : Type w
N : Type ?u.124912
P : Type ?u.124915
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝ : Fin l → M
φ : BoundedFormula L α n
tf : α → Term L β
v : β → M
xs : Fin n → M
⊢ ∀ (n : ℕ) (R : Relations L n) (x : Fin n → M), RelMap (id R) x = RelMap R x
simp