case a.h
n : ℕ
α : TypeVec n
r : α ⊗ α ⟹ repeat n Prop
i : Fin2 n
x : Subtype_ r i
⊢ (toSubtype' r ⊚ ofSubtype' r) i x = id i x
n : ℕ
α : TypeVec n
r : α ⊗ α ⟹ repeat n Prop
⊢ toSubtype' r ⊚ ofSubtype' r = id
ext (i x)
no goals
case a.h
n : ℕ
α : TypeVec n
r : α ⊗ α ⟹ repeat n Prop
i : Fin2 n
x : Subtype_ r i
⊢ (toSubtype' r ⊚ ofSubtype' r) i x = id i x
induction i
<;> dsimp only [id, toSubtype', comp, ofSubtype'] at *
<;> simp [Subtype.eta, *]