Theorem: LO.FirstOrder.UFormula.elim_eq
Proof state before:
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 : σ → γ → γ
p : UFormula L μ
⊢ 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) p =
    WType.elimL (fun p l => LO.FirstOrder.UFormula.F γVerum γFalsum γRel γNrel γAnd γOr γAll γEx x (p, l))
      ((equivW L μ) p)
Tactic:
induction p <;> simp [elim, WType.elimL_mk, F, *]
Proof state after:
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)))

case or
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✝)
⊢ γOr 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✝)) =
    γOr 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)))

case all
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✝)
⊢ γAll 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✝)) =
    γAll 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)

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)