[viraptor]

Could you share an example of such policy? I'm struggling to think of something defined well enough in the real world to apply in Lean.