case a.h
n : ℕ
α : TypeVec n
r : α ⊗ α ⟹ repeat n Prop
i : Fin2 n
x : (fun i => { x // ofRepeat (r i (prod.mk i x.fst x.snd)) }) i
⊢ (subtypeVal r ⊚ toSubtype' r) i x = prod.mk i (↑x).fst (↑x).snd
n : ℕ
α : TypeVec n
r : α ⊗ α ⟹ repeat n Prop
⊢ subtypeVal r ⊚ toSubtype' r = fun i x => prod.mk i (↑x).fst (↑x).snd
ext (i x)
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec n✝} (r : α ⊗ α ⟹ repeat n✝ Prop) (x : { x // ofRepeat (r a✝ (prod.mk a✝ x.fst x.snd)) }),
    subtypeVal r a✝ (toSubtype' r a✝ x) = prod.mk a✝ (↑x).fst (↑x).snd
α : TypeVec (Nat.succ n✝)
r : α ⊗ α ⟹ repeat (Nat.succ n✝) Prop
x : { x // ofRepeat (r (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) x.fst x.snd)) }
⊢ subtypeVal (dropFun r) a✝ (toSubtype' (dropFun r) a✝ x) = prod.mk a✝ (↑x).fst (↑x).snd
case a.h
n : ℕ
α : TypeVec n
r : α ⊗ α ⟹ repeat n Prop
i : Fin2 n
x : (fun i => { x // ofRepeat (r i (prod.mk i x.fst x.snd)) }) i
⊢ (subtypeVal r ⊚ toSubtype' r) i x = prod.mk i (↑x).fst (↑x).snd
induction i <;> dsimp only [id, toSubtype', comp, subtypeVal, prod.mk] at *
no goals
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec n✝} (r : α ⊗ α ⟹ repeat n✝ Prop) (x : { x // ofRepeat (r a✝ (prod.mk a✝ x.fst x.snd)) }),
    subtypeVal r a✝ (toSubtype' r a✝ x) = prod.mk a✝ (↑x).fst (↑x).snd
α : TypeVec (Nat.succ n✝)
r : α ⊗ α ⟹ repeat (Nat.succ n✝) Prop
x : { x // ofRepeat (r (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) x.fst x.snd)) }
⊢ subtypeVal (dropFun r) a✝ (toSubtype' (dropFun r) a✝ x) = prod.mk a✝ (↑x).fst (↑x).snd
simp [*]