Theorem: LO.FirstOrder.UFormula.elim_eq
Proof state before:
case and.e_a.e_fst.e_a
L : Language
μ : Type v
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
inst✝¹ : Primcodable μ
γ : Type u_1
σ : Sort u_2
x : σ
inst✝ : Inhabited γ
γVerum γFalsum : σ → γ
γRel γNrel : σ → (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → γ
γAnd γOr : σ → γ × γ → γ
γAll γEx : σ → γ → γ
a✝¹ a✝ : UFormula L μ
a_ih✝¹ :
  elim (γVerum x) (γFalsum x) (fun {k} f v => γRel x ⟨k, (f, v)⟩) (fun {k} f v => γNrel x ⟨k, (f, v)⟩)
      (fun y₁ y₂ => γAnd x (y₁, y₂)) (fun y₁ y₂ => γOr x (y₁, y₂)) (γAll x) (γEx x) a✝¹ =
    WType.elimL (fun p l => LO.FirstOrder.UFormula.F γVerum γFalsum γRel γNrel γAnd γOr γAll γEx x (p, l))
      ((equivW L μ) a✝¹)
a_ih✝ :
  elim (γVerum x) (γFalsum x) (fun {k} f v => γRel x ⟨k, (f, v)⟩) (fun {k} f v => γNrel x ⟨k, (f, v)⟩)
      (fun y₁ y₂ => γAnd x (y₁, y₂)) (fun y₁ y₂ => γOr x (y₁, y₂)) (γAll x) (γEx x) a✝ =
    WType.elimL (fun p l => LO.FirstOrder.UFormula.F γVerum γFalsum γRel γNrel γAnd γOr γAll γEx x (p, l))
      ((equivW L μ) a✝)
⊢ (equivW L μ) a✝¹ = Bool.rec ((equivW L μ) a✝¹) ((equivW L μ) a✝) (fintypeEquivFin.symm 0)

case and.e_a.e_snd.e_a
L : Language
μ : Type v
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
inst✝¹ : Primcodable μ
γ : Type u_1
σ : Sort u_2
x : σ
inst✝ : Inhabited γ
γVerum γFalsum : σ → γ
γRel γNrel : σ → (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → γ
γAnd γOr : σ → γ × γ → γ
γAll γEx : σ → γ → γ
a✝¹ a✝ : UFormula L μ
a_ih✝¹ :
  elim (γVerum x) (γFalsum x) (fun {k} f v => γRel x ⟨k, (f, v)⟩) (fun {k} f v => γNrel x ⟨k, (f, v)⟩)
      (fun y₁ y₂ => γAnd x (y₁, y₂)) (fun y₁ y₂ => γOr x (y₁, y₂)) (γAll x) (γEx x) a✝¹ =
    WType.elimL (fun p l => LO.FirstOrder.UFormula.F γVerum γFalsum γRel γNrel γAnd γOr γAll γEx x (p, l))
      ((equivW L μ) a✝¹)
a_ih✝ :
  elim (γVerum x) (γFalsum x) (fun {k} f v => γRel x ⟨k, (f, v)⟩) (fun {k} f v => γNrel x ⟨k, (f, v)⟩)
      (fun y₁ y₂ => γAnd x (y₁, y₂)) (fun y₁ y₂ => γOr x (y₁, y₂)) (γAll x) (γEx x) a✝ =
    WType.elimL (fun p l => LO.FirstOrder.UFormula.F γVerum γFalsum γRel γNrel γAnd γOr γAll γEx x (p, l))
      ((equivW L μ) a✝)
⊢ (equivW L μ) a✝ = Bool.rec ((equivW L μ) a✝¹) ((equivW L μ) a✝) (fintypeEquivFin.symm 1)
Tactic:
rw [fintypeEquivFin_symm_zero]
Proof state after:
case and.e_a.e_snd.e_a
L : Language
μ : Type v
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
inst✝¹ : Primcodable μ
γ : Type u_1
σ : Sort u_2
x : σ
inst✝ : Inhabited γ
γVerum γFalsum : σ → γ
γRel γNrel : σ → (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → γ
γAnd γOr : σ → γ × γ → γ
γAll γEx : σ → γ → γ
a✝¹ a✝ : UFormula L μ
a_ih✝¹ :
  elim (γVerum x) (γFalsum x) (fun {k} f v => γRel x ⟨k, (f, v)⟩) (fun {k} f v => γNrel x ⟨k, (f, v)⟩)
      (fun y₁ y₂ => γAnd x (y₁, y₂)) (fun y₁ y₂ => γOr x (y₁, y₂)) (γAll x) (γEx x) a✝¹ =
    WType.elimL (fun p l => LO.FirstOrder.UFormula.F γVerum γFalsum γRel γNrel γAnd γOr γAll γEx x (p, l))
      ((equivW L μ) a✝¹)
a_ih✝ :
  elim (γVerum x) (γFalsum x) (fun {k} f v => γRel x ⟨k, (f, v)⟩) (fun {k} f v => γNrel x ⟨k, (f, v)⟩)
      (fun y₁ y₂ => γAnd x (y₁, y₂)) (fun y₁ y₂ => γOr x (y₁, y₂)) (γAll x) (γEx x) a✝ =
    WType.elimL (fun p l => LO.FirstOrder.UFormula.F γVerum γFalsum γRel γNrel γAnd γOr γAll γEx x (p, l))
      ((equivW L μ) a✝)
⊢ (equivW L μ) a✝ = Bool.rec ((equivW L μ) a✝¹) ((equivW L μ) a✝) (fintypeEquivFin.symm 1)