case h
n✝ : ℕ
c : Composition n✝
n : ℕ
h : 0 < n
i : Fin n
⊢ ↑(↑(embedding (single n h) 0) i) = ↑i
n✝ : ℕ
c : Composition n✝
n : ℕ
h : 0 < n
i : Fin n
⊢ ↑(embedding (single n h) 0) i = i
ext
no goals
case h
n✝ : ℕ
c : Composition n✝
n : ℕ
h : 0 < n
i : Fin n
⊢ ↑(↑(embedding (single n h) 0) i) = ↑i
simp