case nil
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝ : ¬IsPath ps x✝
x : M F
h : ¬IsPath [] x
⊢ iselect [] x = head default

case cons
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝ : ¬IsPath ps x✝
ps_hd : IdxCat F
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → iselect ps_tail x = head default
x : M F
h : ¬IsPath (ps_hd :: ps_tail) x
⊢ iselect (ps_hd :: ps_tail) x = head default
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x : M F
h : ¬IsPath ps x
⊢ iselect ps x = head default
induction' ps with ps_hd ps_tail ps_ih generalizing x
case nil.h
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝ : ¬IsPath ps x✝
x : M F
h : ¬IsPath [] x
⊢ False
case nil
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝ : ¬IsPath ps x✝
x : M F
h : ¬IsPath [] x
⊢ iselect [] x = head default
exfalso
case nil.h
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝ : ¬IsPath ps x✝
x : M F
h : ¬IsPath [] x
⊢ IsPath [] x
case nil.h
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝ : ¬IsPath ps x✝
x : M F
h : ¬IsPath [] x
⊢ False
apply h
no goals
case nil.h
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝ : ¬IsPath ps x✝
x : M F
h : ¬IsPath [] x
⊢ IsPath [] x
constructor
case cons.mk
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → iselect ps_tail x = head default
x : M F
a : F.A
i : B F a
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
⊢ iselect ({ fst := a, snd := i } :: ps_tail) x = head default
case cons
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝ : ¬IsPath ps x✝
ps_hd : IdxCat F
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → iselect ps_tail x = head default
x : M F
h : ¬IsPath (ps_hd :: ps_tail) x
⊢ iselect (ps_hd :: ps_tail) x = head default
cases' ps_hd with a i
case cons.mk.f
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → iselect ps_tail x = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_a : F.A
x_f : B F x_a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := x_a, snd := x_f })
⊢ iselect ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := x_a, snd := x_f }) = head default
case cons.mk
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → iselect ps_tail x = head default
x : M F
a : F.A
i : B F a
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
⊢ iselect ({ fst := a, snd := i } :: ps_tail) x = head default
induction' x using PFunctor.M.casesOn' with x_a x_f
case cons.mk.f
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_a : F.A
x_f : B F x_a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := x_a, snd := x_f })
⊢ head
      (M.casesOn' (M.mk { fst := x_a, snd := x_f }) fun a' f =>
        if h : a = a' then isubtree ps_tail (f (cast (_ : B F a = B F a') i)) else default) =
    head default
case cons.mk.f
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → iselect ps_tail x = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_a : F.A
x_f : B F x_a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := x_a, snd := x_f })
⊢ iselect ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := x_a, snd := x_f }) = head default
simp only [iselect, isubtree] at ps_ih⊢
case pos
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_a : F.A
x_f : B F x_a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := x_a, snd := x_f })
h'' : a = x_a
⊢ head
      (M.casesOn' (M.mk { fst := x_a, snd := x_f }) fun a' f =>
        if h : a = a' then isubtree ps_tail (f (cast (_ : B F a = B F a') i)) else default) =
    head default

case neg
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_a : F.A
x_f : B F x_a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := x_a, snd := x_f })
h'' : ¬a = x_a
⊢ head
      (M.casesOn' (M.mk { fst := x_a, snd := x_f }) fun a' f =>
        if h : a = a' then isubtree ps_tail (f (cast (_ : B F a = B F a') i)) else default) =
    head default
case cons.mk.f
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_a : F.A
x_f : B F x_a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := x_a, snd := x_f })
⊢ head
      (M.casesOn' (M.mk { fst := x_a, snd := x_f }) fun a' f =>
        if h : a = a' then isubtree ps_tail (f (cast (_ : B F a = B F a') i)) else default) =
    head default
by_cases h'' : a = x_a
case pos
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
⊢ head
      (M.casesOn' (M.mk { fst := a, snd := x_f }) fun a' f =>
        if h : a = a' then isubtree ps_tail (f (cast (_ : B F a = B F a') i)) else default) =
    head default

case neg
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_a : F.A
x_f : B F x_a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := x_a, snd := x_f })
h'' : ¬a = x_a
⊢ head
      (M.casesOn' (M.mk { fst := x_a, snd := x_f }) fun a' f =>
        if h : a = a' then isubtree ps_tail (f (cast (_ : B F a = B F a') i)) else default) =
    head default
case pos
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_a : F.A
x_f : B F x_a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := x_a, snd := x_f })
h'' : a = x_a
⊢ head
      (M.casesOn' (M.mk { fst := x_a, snd := x_f }) fun a' f =>
        if h : a = a' then isubtree ps_tail (f (cast (_ : B F a = B F a') i)) else default) =
    head default

case neg
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_a : F.A
x_f : B F x_a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := x_a, snd := x_f })
h'' : ¬a = x_a
⊢ head
      (M.casesOn' (M.mk { fst := x_a, snd := x_f }) fun a' f =>
        if h : a = a' then isubtree ps_tail (f (cast (_ : B F a = B F a') i)) else default) =
    head default
subst x_a
case pos
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
⊢ head (isubtree ps_tail (x_f (cast (_ : B F a = B F a) i))) = head default
case pos
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
⊢ head
      (M.casesOn' (M.mk { fst := a, snd := x_f }) fun a' f =>
        if h : a = a' then isubtree ps_tail (f (cast (_ : B F a = B F a') i)) else default) =
    head default
simp only [dif_pos, eq_self_iff_true, casesOn_mk']
case pos.h
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
⊢ ¬IsPath ps_tail (x_f (cast (_ : B F a = B F a) i))
case pos
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
⊢ head (isubtree ps_tail (x_f (cast (_ : B F a = B F a) i))) = head default
rw [ps_ih]
case pos.h
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
h' : IsPath ps_tail (x_f (cast (_ : B F a = B F a) i))
⊢ False
case pos.h
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
⊢ ¬IsPath ps_tail (x_f (cast (_ : B F a = B F a) i))
intro h'
case pos.h
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
h' : IsPath ps_tail (x_f (cast (_ : B F a = B F a) i))
⊢ IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
case pos.h
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
h' : IsPath ps_tail (x_f (cast (_ : B F a = B F a) i))
⊢ False
apply h
case pos.h.a
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
h' : IsPath ps_tail (x_f (cast (_ : B F a = B F a) i))
⊢ IsPath ps_tail (x_f i)
case pos.h
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
h' : IsPath ps_tail (x_f (cast (_ : B F a = B F a) i))
⊢ IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
constructor <;> try rfl
no goals
case pos.h.a
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
h' : IsPath ps_tail (x_f (cast (_ : B F a = B F a) i))
⊢ IsPath ps_tail (x_f i)
apply h'
case pos.h.a
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
h' : IsPath ps_tail (x_f (cast (_ : B F a = B F a) i))
⊢ IsPath ps_tail (x_f i)
case pos.h.a
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
h' : IsPath ps_tail (x_f (cast (_ : B F a = B F a) i))
⊢ IsPath ps_tail (x_f i)
rfl
no goals
case neg
F : PFunctor
X : Type ?u.22988
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_a : F.A
x_f : B F x_a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := x_a, snd := x_f })
h'' : ¬a = x_a
⊢ head
      (M.casesOn' (M.mk { fst := x_a, snd := x_f }) fun a' f =>
        if h : a = a' then isubtree ps_tail (f (cast (_ : B F a = B F a') i)) else default) =
    head default
simp [*]