case h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x : Fix F α
⊢ rec g x = h x
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
⊢ rec g = h
ext x
case h.h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x : Fix F α
⊢ ∀ (x : F (α ::: Fix F α)),
    (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: fun x => h x) <$$> x → rec g (mk x) = h (mk x)
case h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x : Fix F α
⊢ rec g x = h x
apply Fix.ind_rec
case h.h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x✝ : Fix F α
x : F (α ::: Fix F α)
hyp' : (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: fun x => h x) <$$> x
⊢ rec g (mk x) = h (mk x)
case h.h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x : Fix F α
⊢ ∀ (x : F (α ::: Fix F α)),
    (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: fun x => h x) <$$> x → rec g (mk x) = h (mk x)
intro x hyp'
no goals
case h.h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x✝ : Fix F α
x : F (α ::: Fix F α)
hyp' : (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: fun x => h x) <$$> x
⊢ rec g (mk x) = h (mk x)
rw [hyp, ← hyp', Fix.rec_eq]