F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
u : F α → α
x y : PFunctor.W (P F)
h : Wequiv x y
⊢ recF u x = recF u y
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
u : F α → α
x y : PFunctor.W (P F)
⊢ Wequiv x y → recF u x = recF u y
intro h
case ind
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
u : F α → α
x y : PFunctor.W (P F)
a✝¹ : (P F).A
f✝ f'✝ : PFunctor.B (P F) a✝¹ → PFunctor.W (P F)
a✝ : ∀ (x : PFunctor.B (P F) a✝¹), Wequiv (f✝ x) (f'✝ x)
a_ih✝ : ∀ (x : PFunctor.B (P F) a✝¹), recF u (f✝ x) = recF u (f'✝ x)
⊢ recF u (WType.mk a✝¹ f✝) = recF u (WType.mk a✝¹ f'✝)

case abs
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
u : F α → α
x y : PFunctor.W (P F)
a✝¹ : (P F).A
f✝ : PFunctor.B (P F) a✝¹ → PFunctor.W (P F)
a'✝ : (P F).A
f'✝ : PFunctor.B (P F) a'✝ → PFunctor.W (P F)
a✝ : abs { fst := a✝¹, snd := f✝ } = abs { fst := a'✝, snd := f'✝ }
⊢ recF u (WType.mk a✝¹ f✝) = recF u (WType.mk a'✝ f'✝)

case trans
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
u : F α → α
x y u✝ v✝ w✝ : PFunctor.W (P F)
a✝¹ : Wequiv u✝ v✝
a✝ : Wequiv v✝ w✝
a_ih✝¹ : recF u u✝ = recF u v✝
a_ih✝ : recF u v✝ = recF u w✝
⊢ recF u u✝ = recF u w✝
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
u : F α → α
x y : PFunctor.W (P F)
h : Wequiv x y
⊢ recF u x = recF u y
induction h
case abs
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
u : F α → α
x y : PFunctor.W (P F)
a✝¹ : (P F).A
f✝ : PFunctor.B (P F) a✝¹ → PFunctor.W (P F)
a'✝ : (P F).A
f'✝ : PFunctor.B (P F) a'✝ → PFunctor.W (P F)
a✝ : abs { fst := a✝¹, snd := f✝ } = abs { fst := a'✝, snd := f'✝ }
⊢ recF u (WType.mk a✝¹ f✝) = recF u (WType.mk a'✝ f'✝)

case trans
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
u : F α → α
x y u✝ v✝ w✝ : PFunctor.W (P F)
a✝¹ : Wequiv u✝ v✝
a✝ : Wequiv v✝ w✝
a_ih✝¹ : recF u u✝ = recF u v✝
a_ih✝ : recF u v✝ = recF u w✝
⊢ recF u u✝ = recF u w✝
case ind
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
u : F α → α
x y : PFunctor.W (P F)
a✝¹ : (P F).A
f✝ f'✝ : PFunctor.B (P F) a✝¹ → PFunctor.W (P F)
a✝ : ∀ (x : PFunctor.B (P F) a✝¹), Wequiv (f✝ x) (f'✝ x)
a_ih✝ : ∀ (x : PFunctor.B (P F) a✝¹), recF u (f✝ x) = recF u (f'✝ x)
⊢ recF u (WType.mk a✝¹ f✝) = recF u (WType.mk a✝¹ f'✝)

case abs
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
u : F α → α
x y : PFunctor.W (P F)
a✝¹ : (P F).A
f✝ : PFunctor.B (P F) a✝¹ → PFunctor.W (P F)
a'✝ : (P F).A
f'✝ : PFunctor.B (P F) a'✝ → PFunctor.W (P F)
a✝ : abs { fst := a✝¹, snd := f✝ } = abs { fst := a'✝, snd := f'✝ }
⊢ recF u (WType.mk a✝¹ f✝) = recF u (WType.mk a'✝ f'✝)

case trans
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
u : F α → α
x y u✝ v✝ w✝ : PFunctor.W (P F)
a✝¹ : Wequiv u✝ v✝
a✝ : Wequiv v✝ w✝
a_ih✝¹ : recF u u✝ = recF u v✝
a_ih✝ : recF u v✝ = recF u w✝
⊢ recF u u✝ = recF u w✝
case ind a f f' _ ih => simp only [recF_eq', PFunctor.map_eq, Function.comp, ih]
case trans
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
u : F α → α
x y u✝ v✝ w✝ : PFunctor.W (P F)
a✝¹ : Wequiv u✝ v✝
a✝ : Wequiv v✝ w✝
a_ih✝¹ : recF u u✝ = recF u v✝
a_ih✝ : recF u v✝ = recF u w✝
⊢ recF u u✝ = recF u w✝
case abs
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
u : F α → α
x y : PFunctor.W (P F)
a✝¹ : (P F).A
f✝ : PFunctor.B (P F) a✝¹ → PFunctor.W (P F)
a'✝ : (P F).A
f'✝ : PFunctor.B (P F) a'✝ → PFunctor.W (P F)
a✝ : abs { fst := a✝¹, snd := f✝ } = abs { fst := a'✝, snd := f'✝ }
⊢ recF u (WType.mk a✝¹ f✝) = recF u (WType.mk a'✝ f'✝)

case trans
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
u : F α → α
x y u✝ v✝ w✝ : PFunctor.W (P F)
a✝¹ : Wequiv u✝ v✝
a✝ : Wequiv v✝ w✝
a_ih✝¹ : recF u u✝ = recF u v✝
a_ih✝ : recF u v✝ = recF u w✝
⊢ recF u u✝ = recF u w✝
case abs a f a' f' h => simp only [recF_eq', abs_map, h]
no goals
case trans
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
u : F α → α
x y u✝ v✝ w✝ : PFunctor.W (P F)
a✝¹ : Wequiv u✝ v✝
a✝ : Wequiv v✝ w✝
a_ih✝¹ : recF u u✝ = recF u v✝
a_ih✝ : recF u v✝ = recF u w✝
⊢ recF u u✝ = recF u w✝
case trans x y z _ _ ih₁ ih₂ => exact Eq.trans ih₁ ih₂
no goals
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
u : F α → α
x y : PFunctor.W (P F)
a : (P F).A
f f' : PFunctor.B (P F) a → PFunctor.W (P F)
a✝ : ∀ (x : PFunctor.B (P F) a), Wequiv (f x) (f' x)
ih : ∀ (x : PFunctor.B (P F) a), recF u (f x) = recF u (f' x)
⊢ recF u (WType.mk a f) = recF u (WType.mk a f')
simp only [recF_eq', PFunctor.map_eq, Function.comp, ih]
no goals
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
u : F α → α
x y : PFunctor.W (P F)
a : (P F).A
f : PFunctor.B (P F) a → PFunctor.W (P F)
a' : (P F).A
f' : PFunctor.B (P F) a' → PFunctor.W (P F)
h : abs { fst := a, snd := f } = abs { fst := a', snd := f' }
⊢ recF u (WType.mk a f) = recF u (WType.mk a' f')
simp only [recF_eq', abs_map, h]
no goals
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
u : F α → α
x✝ y✝ x y z : PFunctor.W (P F)
a✝¹ : Wequiv x y
a✝ : Wequiv y z
ih₁ : recF u x = recF u y
ih₂ : recF u y = recF u z
⊢ recF u x = recF u z
exact Eq.trans ih₁ ih₂