no goals
F : PFunctor
X : Type ?u.14033
f : X → Obj F X
x : Obj F (M F)
⊢ Agree (Approx.sMk x 0) (Approx.sMk x (succ 0))
constructor
case a
F : PFunctor
X : Type ?u.14033
f : X → Obj F X
x : Obj F (M F)
n : ℕ
⊢ ∀ (i : B F x.fst), Agree (MIntl.approx (Sigma.snd x i) n) (MIntl.approx (Sigma.snd x i) (succ n))
F : PFunctor
X : Type ?u.14033
f : X → Obj F X
x : Obj F (M F)
n : ℕ
⊢ Agree (Approx.sMk x (succ n)) (Approx.sMk x (succ (succ n)))
constructor
case a
F : PFunctor
X : Type ?u.14033
f : X → Obj F X
x : Obj F (M F)
n : ℕ
i : B F x.fst
⊢ Agree (MIntl.approx (Sigma.snd x i) n) (MIntl.approx (Sigma.snd x i) (succ n))
case a
F : PFunctor
X : Type ?u.14033
f : X → Obj F X
x : Obj F (M F)
n : ℕ
⊢ ∀ (i : B F x.fst), Agree (MIntl.approx (Sigma.snd x i) n) (MIntl.approx (Sigma.snd x i) (succ n))
introv
no goals
case a
F : PFunctor
X : Type ?u.14033
f : X → Obj F X
x : Obj F (M F)
n : ℕ
i : B F x.fst
⊢ Agree (MIntl.approx (Sigma.snd x i) n) (MIntl.approx (Sigma.snd x i) (succ n))
apply (x.2 i).consistent