case mk
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
⊢ ∀ (a : MvPFunctor.W (P F) α), p (Quot.mk Setoid.r a)
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
⊢ ∀ (x : Fix F α), p x
apply Quot.ind
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
⊢ p (Quot.mk Setoid.r x)
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
⊢ ∀ (a : MvPFunctor.W (P F) α), p (Quot.mk Setoid.r a)
intro x
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
⊢ ∀ (a : (P F).A) (f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α)
    (f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α),
    (∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), p (Quot.mk Setoid.r (f i))) →
      p (Quot.mk Setoid.r (MvPFunctor.wMk (P F) a f' f))
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
⊢ p (Quot.mk Setoid.r x)
apply q.P.w_ind _ x
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), p (Quot.mk Setoid.r (f i))
⊢ p (Quot.mk Setoid.r (MvPFunctor.wMk (P F) a f' f))
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
⊢ ∀ (a : (P F).A) (f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α)
    (f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α),
    (∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), p (Quot.mk Setoid.r (f i))) →
      p (Quot.mk Setoid.r (MvPFunctor.wMk (P F) a f' f))
intro a f' f ih
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), p (Quot.mk Setoid.r (f i))
⊢ p (Quotient.mk (wSetoid α) (MvPFunctor.wMk (P F) a f' f))
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), p (Quot.mk Setoid.r (f i))
⊢ p (Quot.mk Setoid.r (MvPFunctor.wMk (P F) a f' f))
change p ⟦q.P.wMk a f' f⟧
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), p (Quot.mk Setoid.r (f i))
⊢ p (mk (abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) }))
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), p (Quot.mk Setoid.r (f i))
⊢ p (Quotient.mk (wSetoid α) (MvPFunctor.wMk (P F) a f' f))
rw [← Fix.ind_aux a f' f]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), p (Quot.mk Setoid.r (f i))
⊢ LiftP (PredLast α p)
    (abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) })
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), p (Quot.mk Setoid.r (f i))
⊢ p (mk (abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) }))
apply h
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), p (Quot.mk Setoid.r (f i))
⊢ ∃ a_1 f_1,
    abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) } =
        abs { fst := a_1, snd := f_1 } ∧
      ∀ (i : Fin2 (n + 1)) (j : MvPFunctor.B (P F) a_1 i), PredLast α p (f_1 i j)
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), p (Quot.mk Setoid.r (f i))
⊢ LiftP (PredLast α p)
    (abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) })
rw [MvQPF.liftP_iff]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), p (Quot.mk Setoid.r (f i))
⊢ ∀ (i : Fin2 (n + 1)) (j : MvPFunctor.B (P F) a i),
    PredLast α p (MvPFunctor.appendContents (P F) f' (fun x => Quotient.mk (wSetoid α) (f x)) i j)
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), p (Quot.mk Setoid.r (f i))
⊢ ∃ a_1 f_1,
    abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) } =
        abs { fst := a_1, snd := f_1 } ∧
      ∀ (i : Fin2 (n + 1)) (j : MvPFunctor.B (P F) a_1 i), PredLast α p (f_1 i j)
refine' ⟨_, _, rfl, _⟩
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), p (Quot.mk Setoid.r (f i))
i : Fin2 (n + 1)
j : MvPFunctor.B (P F) a i
⊢ PredLast α p (MvPFunctor.appendContents (P F) f' (fun x => Quotient.mk (wSetoid α) (f x)) i j)
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), p (Quot.mk Setoid.r (f i))
⊢ ∀ (i : Fin2 (n + 1)) (j : MvPFunctor.B (P F) a i),
    PredLast α p (MvPFunctor.appendContents (P F) f' (fun x => Quotient.mk (wSetoid α) (f x)) i j)
intro i j
case a.fz
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), p (Quot.mk Setoid.r (f i))
j : MvPFunctor.B (P F) a Fin2.fz
⊢ PredLast α p (MvPFunctor.appendContents (P F) f' (fun x => Quotient.mk (wSetoid α) (f x)) Fin2.fz j)

case a.fs
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), p (Quot.mk Setoid.r (f i))
a✝ : Fin2 (Nat.add n 0)
j : MvPFunctor.B (P F) a (Fin2.fs a✝)
⊢ PredLast α p (MvPFunctor.appendContents (P F) f' (fun x => Quotient.mk (wSetoid α) (f x)) (Fin2.fs a✝) j)
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), p (Quot.mk Setoid.r (f i))
i : Fin2 (n + 1)
j : MvPFunctor.B (P F) a i
⊢ PredLast α p (MvPFunctor.appendContents (P F) f' (fun x => Quotient.mk (wSetoid α) (f x)) i j)
cases i
no goals
case a.fz
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), p (Quot.mk Setoid.r (f i))
j : MvPFunctor.B (P F) a Fin2.fz
⊢ PredLast α p (MvPFunctor.appendContents (P F) f' (fun x => Quotient.mk (wSetoid α) (f x)) Fin2.fz j)
apply ih
no goals
case a.fs
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), p (Quot.mk Setoid.r (f i))
a✝ : Fin2 (Nat.add n 0)
j : MvPFunctor.B (P F) a (Fin2.fs a✝)
⊢ PredLast α p (MvPFunctor.appendContents (P F) f' (fun x => Quotient.mk (wSetoid α) (f x)) (Fin2.fs a✝) j)
trivial