case h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x : Fix F
⊢ rec g x = h x
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
⊢ rec g = h
ext x
case h.h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x : Fix F
⊢ ∀ (x : F (Fix F)), rec g <$> x = (fun x => h x) <$> x → rec g (mk x) = h (mk x)
case h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x : Fix F
⊢ rec g x = h x
apply Fix.ind_rec
case h.h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x✝ : Fix F
x : F (Fix F)
hyp' : rec g <$> x = (fun x => h x) <$> x
⊢ rec g (mk x) = h (mk x)
case h.h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x : Fix F
⊢ ∀ (x : F (Fix F)), rec g <$> x = (fun x => h x) <$> x → rec g (mk x) = h (mk x)
intro x hyp'
no goals
case h.h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x✝ : Fix F
x : F (Fix F)
hyp' : rec g <$> x = (fun x => h x) <$> x
⊢ rec g (mk x) = h (mk x)
rw [hyp, ← hyp', Fix.rec_eq]