inj[_+_]_ : (m : ℕ) → (n : ℕ) → Fin (m + n) → Fin m ⊎ Fin n

given Fin (m + n), determine whether it's coming from the "m" part or the "n" part
subset injections and NFA concatenation