Hoare-Logic Style Refinement Types Idris port of Chen, "A Hoare Logic Style Refinement Types Formalisation"