Comment by yorwba

Yes, if you don't mind the repetition or have tooling to deal with it, you can have multiple separate proofs, dependent types won't stop you.