case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
⊢ ∀ (a : PFunctor.W (P F)), p (Quot.mk Setoid.r a)
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
⊢ ∀ (x : Fix F), p x
apply Quot.ind
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
x : PFunctor.W (P F)
⊢ p (Quot.mk Setoid.r x)
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
⊢ ∀ (a : PFunctor.W (P F)), p (Quot.mk Setoid.r a)
intro x
case mk.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), p (Quot.mk Setoid.r (f a))
⊢ p (Quot.mk Setoid.r (WType.mk a f))
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
x : PFunctor.W (P F)
⊢ p (Quot.mk Setoid.r x)
induction' x with a f ih
case mk.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), p (Quot.mk Setoid.r (f a))
⊢ p (Quotient.mk Wsetoid (WType.mk a f))
case mk.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), p (Quot.mk Setoid.r (f a))
⊢ p (Quot.mk Setoid.r (WType.mk a f))
change p ⟦⟨a, f⟩⟧
case mk.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), p (Quot.mk Setoid.r (f a))
⊢ p (mk (abs { fst := a, snd := fun x => Quotient.mk Wsetoid (f x) }))
case mk.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), p (Quot.mk Setoid.r (f a))
⊢ p (Quotient.mk Wsetoid (WType.mk a f))
rw [← Fix.ind_aux a f]
case mk.mk.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), p (Quot.mk Setoid.r (f a))
⊢ Liftp p (abs { fst := a, snd := fun x => Quotient.mk Wsetoid (f x) })
case mk.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), p (Quot.mk Setoid.r (f a))
⊢ p (mk (abs { fst := a, snd := fun x => Quotient.mk Wsetoid (f x) }))
apply h
case mk.mk.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), p (Quot.mk Setoid.r (f a))
⊢ ∃ a_1 f_1,
    abs { fst := a, snd := fun x => Quotient.mk Wsetoid (f x) } = abs { fst := a_1, snd := f_1 } ∧
      ∀ (i : PFunctor.B (P F) a_1), p (f_1 i)
case mk.mk.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), p (Quot.mk Setoid.r (f a))
⊢ Liftp p (abs { fst := a, snd := fun x => Quotient.mk Wsetoid (f x) })
rw [liftp_iff]
case mk.mk.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), p (Quot.mk Setoid.r (f a))
⊢ ∀ (i : PFunctor.B (P F) a), p (Quotient.mk Wsetoid (f i))
case mk.mk.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), p (Quot.mk Setoid.r (f a))
⊢ ∃ a_1 f_1,
    abs { fst := a, snd := fun x => Quotient.mk Wsetoid (f x) } = abs { fst := a_1, snd := f_1 } ∧
      ∀ (i : PFunctor.B (P F) a_1), p (f_1 i)
refine' ⟨_, _, rfl, _⟩
no goals
case mk.mk.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
ih : ∀ (a : PFunctor.B (P F) a), p (Quot.mk Setoid.r (f a))
⊢ ∀ (i : PFunctor.B (P F) a), p (Quotient.mk Wsetoid (f i))
convert ih