n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
r : R x y
⊢ ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
r : R x y
⊢ x = y
apply M.bisim P R _ _ _ r
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
⊢ ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
r : R x y
⊢ ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
clear r x y
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
Hr : R x y
⊢ ∃ a f f₁ f₂,
    dest P x = { fst := a, snd := splitFun f f₁ } ∧
      dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
⊢ ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
introv Hr
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
Hr : R x y
h : (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
⊢ ∃ a f f₁ f₂,
    dest P x = { fst := a, snd := splitFun f f₁ } ∧
      dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
Hr : R x y
⊢ ∃ a f f₁ f₂,
    dest P x = { fst := a, snd := splitFun f f₁ } ∧
      dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
specialize h _ _ Hr
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
h : (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
⊢ ∃ a f f₁ f₂,
    dest P x = { fst := a, snd := splitFun f f₁ } ∧
      dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
Hr : R x y
h : (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
⊢ ∃ a f f₁ f₂,
    dest P x = { fst := a, snd := splitFun f f₁ } ∧
      dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
clear Hr
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
⊢ (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y →
    ∃ a f f₁ f₂,
      dest P x = { fst := a, snd := splitFun f f₁ } ∧
        dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
h : (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
⊢ ∃ a f f₁ f₂,
    dest P x = { fst := a, snd := splitFun f f₁ } ∧
      dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
revert h
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx : B P ax ⟹ α ::: M P α
⊢ (TypeVec.id ::: Quot.mk R) <$$> { fst := ax, snd := fx } = (TypeVec.id ::: Quot.mk R) <$$> dest P y →
    ∃ a f f₁ f₂,
      { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
        dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
⊢ (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y →
    ∃ a f f₁ f₂,
      dest P x = { fst := a, snd := splitFun f f₁ } ∧
        dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
rcases M.dest P x with ⟨ax, fx⟩
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx : B P ax ⟹ α ::: M P α
ay : P.A
fy : B P ay ⟹ α ::: M P α
⊢ (TypeVec.id ::: Quot.mk R) <$$> { fst := ax, snd := fx } = (TypeVec.id ::: Quot.mk R) <$$> { fst := ay, snd := fy } →
    ∃ a f f₁ f₂,
      { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
        { fst := ay, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx : B P ax ⟹ α ::: M P α
⊢ (TypeVec.id ::: Quot.mk R) <$$> { fst := ax, snd := fx } = (TypeVec.id ::: Quot.mk R) <$$> dest P y →
    ∃ a f f₁ f₂,
      { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
        dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
rcases M.dest P y with ⟨ay, fy⟩
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx : B P ax ⟹ α ::: M P α
ay : P.A
fy : B P ay ⟹ α ::: M P α
h : (TypeVec.id ::: Quot.mk R) <$$> { fst := ax, snd := fx } = (TypeVec.id ::: Quot.mk R) <$$> { fst := ay, snd := fy }
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ay, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx : B P ax ⟹ α ::: M P α
ay : P.A
fy : B P ay ⟹ α ::: M P α
⊢ (TypeVec.id ::: Quot.mk R) <$$> { fst := ax, snd := fx } = (TypeVec.id ::: Quot.mk R) <$$> { fst := ay, snd := fy } →
    ∃ a f f₁ f₂,
      { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
        { fst := ay, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
intro h
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx : B P ax ⟹ α ::: M P α
ay : P.A
fy : B P ay ⟹ α ::: M P α
h : { fst := ax, snd := (TypeVec.id ::: Quot.mk R) ⊚ fx } = { fst := ay, snd := (TypeVec.id ::: Quot.mk R) ⊚ fy }
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ay, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx : B P ax ⟹ α ::: M P α
ay : P.A
fy : B P ay ⟹ α ::: M P α
h : (TypeVec.id ::: Quot.mk R) <$$> { fst := ax, snd := fx } = (TypeVec.id ::: Quot.mk R) <$$> { fst := ay, snd := fy }
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ay, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
rw [map_eq, map_eq] at h
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀✝ : Equivalence R
x y : M P α
ax : P.A
fx : B P ax ⟹ α ::: M P α
ay : P.A
fy : B P ay ⟹ α ::: M P α
h₀ : ax = ay
h₁ : HEq ((TypeVec.id ::: Quot.mk R) ⊚ fx) ((TypeVec.id ::: Quot.mk R) ⊚ fy)
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ay, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx : B P ax ⟹ α ::: M P α
ay : P.A
fy : B P ay ⟹ α ::: M P α
h : { fst := ax, snd := (TypeVec.id ::: Quot.mk R) ⊚ fx } = { fst := ay, snd := (TypeVec.id ::: Quot.mk R) ⊚ fy }
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ay, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
injection h with h₀ h₁
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : HEq ((TypeVec.id ::: Quot.mk R) ⊚ fx) ((TypeVec.id ::: Quot.mk R) ⊚ fy)
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ax, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀✝ : Equivalence R
x y : M P α
ax : P.A
fx : B P ax ⟹ α ::: M P α
ay : P.A
fy : B P ay ⟹ α ::: M P α
h₀ : ax = ay
h₁ : HEq ((TypeVec.id ::: Quot.mk R) ⊚ fx) ((TypeVec.id ::: Quot.mk R) ⊚ fy)
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ay, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
subst ay
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ax, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : HEq ((TypeVec.id ::: Quot.mk R) ⊚ fx) ((TypeVec.id ::: Quot.mk R) ⊚ fy)
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ax, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
simp at h₁
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ax, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ax, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
have Hdrop : dropFun fx = dropFun fy := by
  replace h₁ := congr_arg dropFun h₁
  simpa using h₁
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ { fst := ax, snd := fx } = { fst := ax, snd := splitFun (dropFun fx) (lastFun fx) } ∧
    { fst := ax, snd := fy } = { fst := ax, snd := splitFun (dropFun fx) (lastFun fy) } ∧
      ∀ (i : TypeVec.last (B P ax)), R (lastFun fx i) (lastFun fy i)
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ax, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
exists ax, dropFun fx, lastFun fx, lastFun fy
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ { fst := ax, snd := fx } = { fst := ax, snd := fx } ∧
    { fst := ax, snd := fy } = { fst := ax, snd := fy } ∧ ∀ (i : TypeVec.last (B P ax)), R (lastFun fx i) (lastFun fy i)
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ { fst := ax, snd := fx } = { fst := ax, snd := splitFun (dropFun fx) (lastFun fx) } ∧
    { fst := ax, snd := fy } = { fst := ax, snd := splitFun (dropFun fx) (lastFun fy) } ∧
      ∀ (i : TypeVec.last (B P ax)), R (lastFun fx i) (lastFun fy i)
rw [split_dropFun_lastFun, Hdrop, split_dropFun_lastFun]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ ∀ (i : TypeVec.last (B P ax)), R (lastFun fx i) (lastFun fy i)
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ { fst := ax, snd := fx } = { fst := ax, snd := fx } ∧
    { fst := ax, snd := fy } = { fst := ax, snd := fy } ∧ ∀ (i : TypeVec.last (B P ax)), R (lastFun fx i) (lastFun fy i)
simp
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
i : TypeVec.last (B P ax)
⊢ R (lastFun fx i) (lastFun fy i)
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ ∀ (i : TypeVec.last (B P ax)), R (lastFun fx i) (lastFun fy i)
intro i
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
Hdrop : dropFun fx = dropFun fy
i : TypeVec.last (B P ax)
h₁ : ((TypeVec.id ::: Quot.mk R) ⊚ fx) Fin2.fz i = ((TypeVec.id ::: Quot.mk R) ⊚ fy) Fin2.fz i
⊢ R (lastFun fx i) (lastFun fy i)
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
i : TypeVec.last (B P ax)
⊢ R (lastFun fx i) (lastFun fy i)
replace h₁ := congr_fun (congr_fun h₁ Fin2.fz) i
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
Hdrop : dropFun fx = dropFun fy
i : TypeVec.last (B P ax)
h₁ : EqvGen R (fx Fin2.fz i) (fy Fin2.fz i)
⊢ R (lastFun fx i) (lastFun fy i)
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
Hdrop : dropFun fx = dropFun fy
i : TypeVec.last (B P ax)
h₁ : Quot.mk R (fx Fin2.fz i) = Quot.mk R (fy Fin2.fz i)
⊢ R (lastFun fx i) (lastFun fy i)
replace h₁ := Quot.exact _ h₁
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
Hdrop : dropFun fx = dropFun fy
i : TypeVec.last (B P ax)
h₁ : R (fx Fin2.fz i) (fy Fin2.fz i)
⊢ R (lastFun fx i) (lastFun fy i)
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
Hdrop : dropFun fx = dropFun fy
i : TypeVec.last (B P ax)
h₁ : EqvGen R (fx Fin2.fz i) (fy Fin2.fz i)
⊢ R (lastFun fx i) (lastFun fy i)
rw [h₀.eqvGen_iff] at h₁
no goals
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
Hdrop : dropFun fx = dropFun fy
i : TypeVec.last (B P ax)
h₁ : R (fx Fin2.fz i) (fy Fin2.fz i)
⊢ R (lastFun fx i) (lastFun fy i)
exact h₁
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : dropFun ((TypeVec.id ::: Quot.mk R) ⊚ fx) = dropFun ((TypeVec.id ::: Quot.mk R) ⊚ fy)
⊢ dropFun fx = dropFun fy
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
⊢ dropFun fx = dropFun fy
replace h₁ := congr_arg dropFun h₁
no goals
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : dropFun ((TypeVec.id ::: Quot.mk R) ⊚ fx) = dropFun ((TypeVec.id ::: Quot.mk R) ⊚ fy)
⊢ dropFun fx = dropFun fy
simpa using h₁