rw [h₀]
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).fst) <$>
        (fun a =>
            { val := (construct (destruct a), a),
              property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
          destruct y =
      destruct x ∧
    (fun x => (↑x).snd) <$>
        (fun a =>
            { val := (construct (destruct a), a),
              property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
          destruct y =
      destruct y
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).fst) <$>
        (fun a =>
            { val := (construct (destruct a), a),
              property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
          destruct y =
      (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y ∧
    (fun x => (↑x).snd) <$>
        (fun a =>
            { val := (construct (destruct a), a),
              property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
          destruct y =
      destruct y