-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x_1 : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun (a b : Cofix F α) ↦
    ∃ (x : Cofix F α),
      a =
          corec (F := F) (α := α) (β := Cofix F α ⊕ β)
            (Function.comp (β := F (α ::: (Cofix F α ⊕ β)))
              (MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: (Cofix F α ⊕ β))
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Cofix F α ⊕ β) ↦ x))
              (Sum.rec (motive := fun (x : Cofix F α ⊕ β) ↦ F (α ::: (Cofix F α ⊕ β)))
                (fun (val : Cofix F α) ↦
                  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) (val.dest (F := F) (α := α)))
                fun (val : β) ↦ g val))
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec (F := F) (α := α) (β := Cofix F α ⊕ β)
      (Function.comp (β := F (α ::: (Cofix F α ⊕ β)))
        (MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: (Cofix F α ⊕ β))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Cofix F α ⊕ β) ↦ x))
        (Sum.rec (motive := fun (x : Cofix F α ⊕ β) ↦ F (α ::: (Cofix F α ⊕ β)))
          (fun (val : Cofix F α) ↦
            MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
              (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) (val.dest (F := F) (α := α)))
          fun (val : β) ↦ g val))
      (Sum.inl x)
Hb : b = x
h :
  ∀ (x : Cofix F α),
    R
      (corec (F := F) (α := α)
        (fun (x : Cofix F α ⊕ β) ↦
          MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: (Cofix F α ⊕ β))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Cofix F α ⊕ β) ↦ x)
            (Sum.rec (motive := fun (x : Cofix F α ⊕ β) ↦ F (α ::: (Cofix F α ⊕ β)))
              (fun (val : Cofix F α) ↦
                MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
                  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) (val.dest (F := F) (α := α)))
              (fun (val : β) ↦ g val) x))
        (Sum.inl x))
      x
⊢ ∀ (x : Cofix F α),
    R
      (Function.comp (β := Cofix F α ⊕ β)
        (Function.comp (β := Cofix F α ⊕ β)
          (corec (F := F) (α := α) fun (x : Cofix F α ⊕ β) ↦
            MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: (Cofix F α ⊕ β))
              (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Cofix F α ⊕ β) ↦ x)
              (Sum.rec (motive := fun (x : Cofix F α ⊕ β) ↦ F (α ::: (Cofix F α ⊕ β)))
                (fun (val : Cofix F α) ↦
                  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) (val.dest (F := F) (α := α)))
                (fun (val : β) ↦ g val) x))
          fun (x : Cofix F α ⊕ β) ↦ x)
        Sum.inl x)
      x

Tactic:
dsimp [Function.comp_def]

Premises used: Function.comp_def