Theorems · Theorem · logic and foundations

PFun.fixInduction.congr_simp

∀ {α : Type u_1} {β : Type u_2} {C : α → Sort u_7} {f : α →. β ⊕ α} {b : β} {a : α} (h : b ∈ f.fix a)
  (H H_1 : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'),
  H = H_1 → PFun.fixInduction h H = PFun.fixInduction h H_1

Defined in

Mathlib.Data.PFun

Cited by

0 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound