exact this.of_eq (fun p q => by simp; rw [fintypeEquivFin_false, fintypeEquivFin_true]; simp)
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 μ
this✝ :
  Primrec₂ fun x w =>
    WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) x) ((fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])
this :
  Primrec₂ fun a b =>
    (equivW L μ).symm
      (WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) ())
        ((fintypeArrowEquivFinArrow' ⋯).symm
          ![(id ((equivW L μ) a, (equivW L μ) b)).1, (id ((equivW L μ) a, (equivW L μ) b)).2]))
⊢ Primrec₂ and
no goals