Logical relations for coherence of effect subtyping

All formalizations are built on the IxFree library.