wip: observation interval proofs

Merge request from branch oio which includes notion of offset (which wasn't there in the original OI MR).

(* Why the branch name oio?

=> I wanted to name it so that it represents "OI with offset included", so I thought of naming oi_offset but this would be too long to write frequent commit messages, so I shortened it to oio. *)