congr
case ex
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✝ : 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✝)
⊢ γEx 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✝)) =
    γEx x
      (fintypeArrowEquivFinArrow
        (fun b =>
          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✝))
        0)
no goals