n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
x : W P α
⊢ C x
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
⊢ ∀ (x : W P α), C x
intro x
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
a : (wp P).A
f : B (wp P) a ⟹ α
⊢ C { fst := a, snd := f }
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
x : W P α
⊢ C x
cases' x with a f
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
a : (wp P).A
f : B (wp P) a ⟹ α
⊢ ∀ (a : P.A) (f : PFunctor.B (last P) a → PFunctor.W (last P)) (f' : WPath P (WType.mk a f) ⟹ α),
    (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
      C { fst := WType.mk a f, snd := f' }
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
a : (wp P).A
f : B (wp P) a ⟹ α
⊢ C { fst := a, snd := f }
apply @wp_ind n P α fun a f => C ⟨a, f⟩
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
a : (wp P).A
f : B (wp P) a ⟹ α
⊢ ∀ (a : P.A) (f : PFunctor.B (last P) a → PFunctor.W (last P)) (f' : WPath P (WType.mk a f) ⟹ α),
    (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
      C { fst := WType.mk a f, snd := f' }
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
a : (wp P).A
f : B (wp P) a ⟹ α
⊢ ∀ (a : P.A) (f : PFunctor.B (last P) a → PFunctor.W (last P)) (f' : WPath P (WType.mk a f) ⟹ α),
    (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
      C { fst := WType.mk a f, snd := f' }
dsimp
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
⊢ C { fst := WType.mk a f, snd := f' }
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
a : (wp P).A
f : B (wp P) a ⟹ α
⊢ ∀ (a : P.A) (f : PFunctor.B (last P) a → PFunctor.W (last P)) (f' : WPath P (WType.mk a f) ⟹ α),
    (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
      C { fst := WType.mk a f, snd := f' }
intro a f f' ih'
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) →
      C { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd }
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
⊢ C { fst := WType.mk a f, snd := f' }
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
⊢ C { fst := WType.mk a f, snd := f' }
dsimp [wMk] at ih
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) →
      C { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd }
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
ih'' : (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
  C
    { fst := WType.mk a fun i => { fst := f i, snd := wPathDestRight P f' i }.fst,
      snd := wPathCasesOn P (wPathDestLeft P f') fun i => { fst := f i, snd := wPathDestRight P f' i }.snd } :=
  ih a (wPathDestLeft P f') fun i => { fst := f i, snd := wPathDestRight P f' i }
⊢ C { fst := WType.mk a f, snd := f' }
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) →
      C { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd }
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
⊢ C { fst := WType.mk a f, snd := f' }
let ih'' := ih a (P.wPathDestLeft f') fun i => ⟨f i, P.wPathDestRight f' i⟩
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) →
      C { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd }
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
ih'' : (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
  C { fst := WType.mk a fun i => f i, snd := wPathCasesOn P (wPathDestLeft P f') fun i => wPathDestRight P f' i } :=
  ih a (wPathDestLeft P f') fun i => { fst := f i, snd := wPathDestRight P f' i }
⊢ C { fst := WType.mk a f, snd := f' }
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) →
      C { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd }
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
ih'' : (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
  C
    { fst := WType.mk a fun i => { fst := f i, snd := wPathDestRight P f' i }.fst,
      snd := wPathCasesOn P (wPathDestLeft P f') fun i => { fst := f i, snd := wPathDestRight P f' i }.snd } :=
  ih a (wPathDestLeft P f') fun i => { fst := f i, snd := wPathDestRight P f' i }
⊢ C { fst := WType.mk a f, snd := f' }
dsimp at ih''
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) →
      C { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd }
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
ih'' :
  (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
    C { fst := WType.mk a fun i => f i, snd := f' }
⊢ C { fst := WType.mk a f, snd := f' }
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) →
      C { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd }
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
ih'' : (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
  C { fst := WType.mk a fun i => f i, snd := wPathCasesOn P (wPathDestLeft P f') fun i => wPathDestRight P f' i } :=
  ih a (wPathDestLeft P f') fun i => { fst := f i, snd := wPathDestRight P f' i }
⊢ C { fst := WType.mk a f, snd := f' }
rw [wPathCasesOn_eta] at ih''
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) →
      C { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd }
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
ih'' :
  (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
    C { fst := WType.mk a fun i => f i, snd := f' }
⊢ ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) →
      C { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd }
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
ih'' :
  (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
    C { fst := WType.mk a fun i => f i, snd := f' }
⊢ C { fst := WType.mk a f, snd := f' }
apply ih''
no goals
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) →
      C { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd }
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
ih'' :
  (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
    C { fst := WType.mk a fun i => f i, snd := f' }
⊢ ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
apply ih'