no goals
n : ℕ
c : Composition n
i : Fin (length c)
j : Fin (blocksFun c i)
⊢ ↑(invEmbedding c (↑(embedding c i) j)) = ↑j
simp_rw [coe_invEmbedding, index_embedding, coe_embedding, add_tsub_cancel_left]