LLFp: A logical framework for modeling external evidence, side conditions, and proof irrelevance using monads