casesOn_mk' — Mathlib

English

For any F and x : M F, head'(x.approx (succ n)) = head'(x.approx (succ m)).

Русский

Для любого F и x ∈ M F, head'(x.approx (succ n)) = head'(x.approx (succ m)).

LaTeX

$$$\\forall F,\\forall n,m:\\mathbb{N},\\; head'(x.approx(\\operatorname{succ} n)) = head'(x.approx(\\operatorname{succ} m))$$$

Lean4

@[simp]
theorem casesOn_mk' {r : M F → Sort*} {a} (x : F.B a → M F) (f : ∀ (a) (f : F.B a → M F), r (M.mk ⟨a, f⟩)) :
    PFunctor.M.casesOn' (M.mk ⟨a, x⟩) f = f a x :=
  @cases_mk F r ⟨a, x⟩ (fun ⟨a, g⟩ => f a g)

Похожие утверждения