case zero
F : PFunctor
X : Type w
f : X → Obj F X
i✝ i : X
⊢ Agree (sCorec f i zero) (sCorec f i (succ zero))

case succ
F : PFunctor
X : Type w
f : X → Obj F X
i✝ : X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i (succ n))
i : X
⊢ Agree (sCorec f i (succ n)) (sCorec f i (succ (succ n)))
F : PFunctor
X : Type w
f : X → Obj F X
i : X
n : ℕ
⊢ Agree (sCorec f i n) (sCorec f i (succ n))
induction' n with n n_ih generalizing i
case succ
F : PFunctor
X : Type w
f : X → Obj F X
i✝ : X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i (succ n))
i : X
⊢ Agree (sCorec f i (succ n)) (sCorec f i (succ (succ n)))
case zero
F : PFunctor
X : Type w
f : X → Obj F X
i✝ i : X
⊢ Agree (sCorec f i zero) (sCorec f i (succ zero))

case succ
F : PFunctor
X : Type w
f : X → Obj F X
i✝ : X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i (succ n))
i : X
⊢ Agree (sCorec f i (succ n)) (sCorec f i (succ (succ n)))
constructor
case succ.mk
F : PFunctor
X : Type w
f : X → Obj F X
i✝ : X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i (succ n))
i : X
y : F.A
g : B F y → X
h : f i = { fst := y, snd := g }
⊢ Agree (sCorec f i (succ n)) (sCorec f i (succ (succ n)))
case succ
F : PFunctor
X : Type w
f : X → Obj F X
i✝ : X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i (succ n))
i : X
⊢ Agree (sCorec f i (succ n)) (sCorec f i (succ (succ n)))
cases' h : f i with y g
case succ.mk.a
F : PFunctor
X : Type w
f : X → Obj F X
i✝ : X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i (succ n))
i : X
y : F.A
g : B F y → X
h : f i = { fst := y, snd := g }
⊢ ∀ (i_1 : B F (f i).fst), Agree (sCorec f (Sigma.snd (f i) i_1) n) (sCorec f (Sigma.snd (f i) i_1) (succ n))
case succ.mk
F : PFunctor
X : Type w
f : X → Obj F X
i✝ : X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i (succ n))
i : X
y : F.A
g : B F y → X
h : f i = { fst := y, snd := g }
⊢ Agree (sCorec f i (succ n)) (sCorec f i (succ (succ n)))
constructor
case succ.mk.a
F : PFunctor
X : Type w
f : X → Obj F X
i✝¹ : X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i (succ n))
i✝ : X
y : F.A
g : B F y → X
h : f i✝ = { fst := y, snd := g }
i : B F (f i✝).fst
⊢ Agree (sCorec f (Sigma.snd (f i✝) i) n) (sCorec f (Sigma.snd (f i✝) i) (succ n))
case succ.mk.a
F : PFunctor
X : Type w
f : X → Obj F X
i✝ : X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i (succ n))
i : X
y : F.A
g : B F y → X
h : f i = { fst := y, snd := g }
⊢ ∀ (i_1 : B F (f i).fst), Agree (sCorec f (Sigma.snd (f i) i_1) n) (sCorec f (Sigma.snd (f i) i_1) (succ n))
introv
no goals
case succ.mk.a
F : PFunctor
X : Type w
f : X → Obj F X
i✝¹ : X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i (succ n))
i✝ : X
y : F.A
g : B F y → X
h : f i✝ = { fst := y, snd := g }
i : B F (f i✝).fst
⊢ Agree (sCorec f (Sigma.snd (f i✝) i) n) (sCorec f (Sigma.snd (f i✝) i) (succ n))
apply n_ih