Theorem: LO.FirstOrder.UFormula.elim_eq
Proof state before:
case and
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✝)
⊢ γAnd x
      (WType.elimL
          (fun p l =>
            Sum.rec (fun val => bif p.1 then γRel x val else γNrel x val)
              (fun val =>
                Sum.rec (fun val => bif p.1 then γVerum x else γFalsum x)
                  (fun val =>
                    Sum.rec (fun val => bif p.1 then γAnd x (l.getI 0, l.getI 1) else γOr x (l.getI 0, l.getI 1))
                      (fun val => bif p.1 then γAll x (l.getI 0) else γEx x (l.getI 0)) val)
                  val)
              p.2)
          ((equivW L μ) a✝¹),
        WType.elimL
          (fun p l =>
            Sum.rec (fun val => bif p.1 then γRel x val else γNrel x val)
              (fun val =>
                Sum.rec (fun val => bif p.1 then γVerum x else γFalsum x)
                  (fun val =>
                    Sum.rec (fun val => bif p.1 then γAnd x (l.getI 0, l.getI 1) else γOr x (l.getI 0, l.getI 1))
                      (fun val => bif p.1 then γAll x (l.getI 0) else γEx x (l.getI 0)) val)
                  val)
              p.2)
          ((equivW L μ) a✝)) =
    γAnd x
      (WType.elimL
          (fun p l =>
            Sum.rec (fun val => bif p.1 then γRel x val else γNrel x val)
              (fun val =>
                Sum.rec (fun val => bif p.1 then γVerum x else γFalsum x)
                  (fun val =>
                    Sum.rec (fun val => bif p.1 then γAnd x (l.getI 0, l.getI 1) else γOr x (l.getI 0, l.getI 1))
                      (fun val => bif p.1 then γAll x (l.getI 0) else γEx x (l.getI 0)) val)
                  val)
              p.2)
          (Bool.rec ((equivW L μ) a✝¹) ((equivW L μ) a✝) (fintypeEquivFin.symm 0)),
        WType.elimL
          (fun p l =>
            Sum.rec (fun val => bif p.1 then γRel x val else γNrel x val)
              (fun val =>
                Sum.rec (fun val => bif p.1 then γVerum x else γFalsum x)
                  (fun val =>
                    Sum.rec (fun val => bif p.1 then γAnd x (l.getI 0, l.getI 1) else γOr x (l.getI 0, l.getI 1))
                      (fun val => bif p.1 then γAll x (l.getI 0) else γEx x (l.getI 0)) val)
                  val)
              p.2)
          (Bool.rec ((equivW L μ) a✝¹) ((equivW L μ) a✝) (fintypeEquivFin.symm 1)))
Tactic:
congr
Proof state after:
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)