case a.h
n : ℕ
α : TypeVec n
p : α ⟹ repeat n Prop
i : Fin2 n
x : Subtype_ p i
⊢ (toSubtype p ⊚ ofSubtype p) i x = id i x
n : ℕ
α : TypeVec n
p : α ⟹ repeat n Prop
⊢ toSubtype p ⊚ ofSubtype p = id
ext (i x)
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec n✝} (p : α ⟹ repeat n✝ Prop) (x : Subtype_ p a✝), toSubtype p a✝ (ofSubtype p a✝ x) = x
α : TypeVec (Nat.succ n✝)
p : α ⟹ repeat (Nat.succ n✝) Prop
x : Subtype_ p (Fin2.fs a✝)
⊢ toSubtype (dropFun p) a✝ (ofSubtype (dropFun p) a✝ x) = x
case a.h
n : ℕ
α : TypeVec n
p : α ⟹ repeat n Prop
i : Fin2 n
x : Subtype_ p i
⊢ (toSubtype p ⊚ ofSubtype p) i x = id i x
induction i <;> dsimp only [id, toSubtype, comp, ofSubtype] at *
no goals
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec n✝} (p : α ⟹ repeat n✝ Prop) (x : Subtype_ p a✝), toSubtype p a✝ (ofSubtype p a✝ x) = x
α : TypeVec (Nat.succ n✝)
p : α ⟹ repeat (Nat.succ n✝) Prop
x : Subtype_ p (Fin2.fs a✝)
⊢ toSubtype (dropFun p) a✝ (ofSubtype (dropFun p) a✝ x) = x
simp [*]