m n : ℕ
α : Fin (n + 1) → Type u
x✝ : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
P : ((i : Fin (Nat.succ n)) → α i) → Sort v
h : (x₀ : α 0) → (x : (i : Fin n) → α (succ i)) → P (cons x₀ x)
x₀ : α 0
x : (i : Fin n) → α (succ i)
⊢ h (cons x₀ x 0) (tail (cons x₀ x)) = h x₀ x
m n : ℕ
α : Fin (n + 1) → Type u
x✝ : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
P : ((i : Fin (Nat.succ n)) → α i) → Sort v
h : (x₀ : α 0) → (x : (i : Fin n) → α (succ i)) → P (cons x₀ x)
x₀ : α 0
x : (i : Fin n) → α (succ i)
⊢ consCases h (cons x₀ x) = h x₀ x
rw [consCases, cast_eq]
no goals
m n : ℕ
α : Fin (n + 1) → Type u
x✝ : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y : α (succ i)
z : α 0
P : ((i : Fin (Nat.succ n)) → α i) → Sort v
h : (x₀ : α 0) → (x : (i : Fin n) → α (succ i)) → P (cons x₀ x)
x₀ : α 0
x : (i : Fin n) → α (succ i)
⊢ h (cons x₀ x 0) (tail (cons x₀ x)) = h x₀ x
congr