Different but equivalent type in function input

Stream: general

[Jamie Reason]

Hey, I had a function input which requires a term of type matrix fin (n+1) fin (n+1) D but it was failing because I only have a term of type matrix (fin 1 ⊕ fin n) (fin 1 ⊕ fin n) D. fin_sum_fin_equiv gives equivalence between fin 1 ⊕ fin n and fin (n+1), but how do I use this?

[Eric Wieser]

Via docs#matrix.reindex