n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : MvPFunctor.W (P F) α
h : WEquiv x y
⊢ WEquiv y x
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : MvPFunctor.W (P F) α
⊢ WEquiv x y → WEquiv y x
intro h
case ind
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : MvPFunctor.W (P F) α
a✝¹ : (P F).A
f'✝ : MvPFunctor.B (MvPFunctor.drop (P F)) a✝¹ ⟹ α
f₀✝ f₁✝ : PFunctor.B (MvPFunctor.last (P F)) a✝¹ → MvPFunctor.W (P F) α
a✝ : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a✝¹), WEquiv (f₀✝ x) (f₁✝ x)
a_ih✝ : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a✝¹), WEquiv (f₁✝ x) (f₀✝ x)
⊢ WEquiv (MvPFunctor.wMk (P F) a✝¹ f'✝ f₁✝) (MvPFunctor.wMk (P F) a✝¹ f'✝ f₀✝)

case abs
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : MvPFunctor.W (P F) α
a₀✝ : (P F).A
f'₀✝ : MvPFunctor.B (MvPFunctor.drop (P F)) a₀✝ ⟹ α
f₀✝ : PFunctor.B (MvPFunctor.last (P F)) a₀✝ → MvPFunctor.W (P F) α
a₁✝ : (P F).A
f'₁✝ : MvPFunctor.B (MvPFunctor.drop (P F)) a₁✝ ⟹ α
f₁✝ : PFunctor.B (MvPFunctor.last (P F)) a₁✝ → MvPFunctor.W (P F) α
a✝ :
  abs { fst := a₀✝, snd := MvPFunctor.appendContents (P F) f'₀✝ f₀✝ } =
    abs { fst := a₁✝, snd := MvPFunctor.appendContents (P F) f'₁✝ f₁✝ }
⊢ WEquiv (MvPFunctor.wMk (P F) a₁✝ f'₁✝ f₁✝) (MvPFunctor.wMk (P F) a₀✝ f'₀✝ f₀✝)

case trans
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y u✝ v✝ w✝ : MvPFunctor.W (P F) α
a✝¹ : WEquiv u✝ v✝
a✝ : WEquiv v✝ w✝
a_ih✝¹ : WEquiv v✝ u✝
a_ih✝ : WEquiv w✝ v✝
⊢ WEquiv w✝ u✝
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : MvPFunctor.W (P F) α
h : WEquiv x y
⊢ WEquiv y x
induction h
case abs
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : MvPFunctor.W (P F) α
a₀✝ : (P F).A
f'₀✝ : MvPFunctor.B (MvPFunctor.drop (P F)) a₀✝ ⟹ α
f₀✝ : PFunctor.B (MvPFunctor.last (P F)) a₀✝ → MvPFunctor.W (P F) α
a₁✝ : (P F).A
f'₁✝ : MvPFunctor.B (MvPFunctor.drop (P F)) a₁✝ ⟹ α
f₁✝ : PFunctor.B (MvPFunctor.last (P F)) a₁✝ → MvPFunctor.W (P F) α
a✝ :
  abs { fst := a₀✝, snd := MvPFunctor.appendContents (P F) f'₀✝ f₀✝ } =
    abs { fst := a₁✝, snd := MvPFunctor.appendContents (P F) f'₁✝ f₁✝ }
⊢ WEquiv (MvPFunctor.wMk (P F) a₁✝ f'₁✝ f₁✝) (MvPFunctor.wMk (P F) a₀✝ f'₀✝ f₀✝)

case trans
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y u✝ v✝ w✝ : MvPFunctor.W (P F) α
a✝¹ : WEquiv u✝ v✝
a✝ : WEquiv v✝ w✝
a_ih✝¹ : WEquiv v✝ u✝
a_ih✝ : WEquiv w✝ v✝
⊢ WEquiv w✝ u✝
case ind
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : MvPFunctor.W (P F) α
a✝¹ : (P F).A
f'✝ : MvPFunctor.B (MvPFunctor.drop (P F)) a✝¹ ⟹ α
f₀✝ f₁✝ : PFunctor.B (MvPFunctor.last (P F)) a✝¹ → MvPFunctor.W (P F) α
a✝ : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a✝¹), WEquiv (f₀✝ x) (f₁✝ x)
a_ih✝ : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a✝¹), WEquiv (f₁✝ x) (f₀✝ x)
⊢ WEquiv (MvPFunctor.wMk (P F) a✝¹ f'✝ f₁✝) (MvPFunctor.wMk (P F) a✝¹ f'✝ f₀✝)

case abs
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : MvPFunctor.W (P F) α
a₀✝ : (P F).A
f'₀✝ : MvPFunctor.B (MvPFunctor.drop (P F)) a₀✝ ⟹ α
f₀✝ : PFunctor.B (MvPFunctor.last (P F)) a₀✝ → MvPFunctor.W (P F) α
a₁✝ : (P F).A
f'₁✝ : MvPFunctor.B (MvPFunctor.drop (P F)) a₁✝ ⟹ α
f₁✝ : PFunctor.B (MvPFunctor.last (P F)) a₁✝ → MvPFunctor.W (P F) α
a✝ :
  abs { fst := a₀✝, snd := MvPFunctor.appendContents (P F) f'₀✝ f₀✝ } =
    abs { fst := a₁✝, snd := MvPFunctor.appendContents (P F) f'₁✝ f₁✝ }
⊢ WEquiv (MvPFunctor.wMk (P F) a₁✝ f'₁✝ f₁✝) (MvPFunctor.wMk (P F) a₀✝ f'₀✝ f₀✝)

case trans
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y u✝ v✝ w✝ : MvPFunctor.W (P F) α
a✝¹ : WEquiv u✝ v✝
a✝ : WEquiv v✝ w✝
a_ih✝¹ : WEquiv v✝ u✝
a_ih✝ : WEquiv w✝ v✝
⊢ WEquiv w✝ u✝
case ind a f' f₀ f₁ _h ih => exact WEquiv.ind _ _ _ _ ih
case trans
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y u✝ v✝ w✝ : MvPFunctor.W (P F) α
a✝¹ : WEquiv u✝ v✝
a✝ : WEquiv v✝ w✝
a_ih✝¹ : WEquiv v✝ u✝
a_ih✝ : WEquiv w✝ v✝
⊢ WEquiv w✝ u✝
case abs
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : MvPFunctor.W (P F) α
a₀✝ : (P F).A
f'₀✝ : MvPFunctor.B (MvPFunctor.drop (P F)) a₀✝ ⟹ α
f₀✝ : PFunctor.B (MvPFunctor.last (P F)) a₀✝ → MvPFunctor.W (P F) α
a₁✝ : (P F).A
f'₁✝ : MvPFunctor.B (MvPFunctor.drop (P F)) a₁✝ ⟹ α
f₁✝ : PFunctor.B (MvPFunctor.last (P F)) a₁✝ → MvPFunctor.W (P F) α
a✝ :
  abs { fst := a₀✝, snd := MvPFunctor.appendContents (P F) f'₀✝ f₀✝ } =
    abs { fst := a₁✝, snd := MvPFunctor.appendContents (P F) f'₁✝ f₁✝ }
⊢ WEquiv (MvPFunctor.wMk (P F) a₁✝ f'₁✝ f₁✝) (MvPFunctor.wMk (P F) a₀✝ f'₀✝ f₀✝)

case trans
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y u✝ v✝ w✝ : MvPFunctor.W (P F) α
a✝¹ : WEquiv u✝ v✝
a✝ : WEquiv v✝ w✝
a_ih✝¹ : WEquiv v✝ u✝
a_ih✝ : WEquiv w✝ v✝
⊢ WEquiv w✝ u✝
case abs a₀ f'₀ f₀ a₁ f'₁ f₁ h => exact WEquiv.abs _ _ _ _ _ _ h.symm
no goals
case trans
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y u✝ v✝ w✝ : MvPFunctor.W (P F) α
a✝¹ : WEquiv u✝ v✝
a✝ : WEquiv v✝ w✝
a_ih✝¹ : WEquiv v✝ u✝
a_ih✝ : WEquiv w✝ v✝
⊢ WEquiv w✝ u✝
case trans x y z _e₁ _e₂ ih₁ ih₂ => exact MvQPF.WEquiv.trans _ _ _ ih₂ ih₁
no goals
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
_h : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (f₁ x) (f₀ x)
⊢ WEquiv (MvPFunctor.wMk (P F) a f' f₁) (MvPFunctor.wMk (P F) a f' f₀)
exact WEquiv.ind _ _ _ _ ih
no goals
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : MvPFunctor.W (P F) α
a₀ : (P F).A
f'₀ : MvPFunctor.B (MvPFunctor.drop (P F)) a₀ ⟹ α
f₀ : PFunctor.B (MvPFunctor.last (P F)) a₀ → MvPFunctor.W (P F) α
a₁ : (P F).A
f'₁ : MvPFunctor.B (MvPFunctor.drop (P F)) a₁ ⟹ α
f₁ : PFunctor.B (MvPFunctor.last (P F)) a₁ → MvPFunctor.W (P F) α
h :
  abs { fst := a₀, snd := MvPFunctor.appendContents (P F) f'₀ f₀ } =
    abs { fst := a₁, snd := MvPFunctor.appendContents (P F) f'₁ f₁ }
⊢ WEquiv (MvPFunctor.wMk (P F) a₁ f'₁ f₁) (MvPFunctor.wMk (P F) a₀ f'₀ f₀)
exact WEquiv.abs _ _ _ _ _ _ h.symm
no goals
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ y✝ x y z : MvPFunctor.W (P F) α
_e₁ : WEquiv x y
_e₂ : WEquiv y z
ih₁ : WEquiv y x
ih₂ : WEquiv z y
⊢ WEquiv z x
exact MvQPF.WEquiv.trans _ _ _ ih₂ ih₁