2386 

  2386   \medskip

  2387   %\medskip

  2387 

  2388 

  2388   \noindent {\bf Acknowledgements:} We are grateful for the comments

  2389   %\noindent

  2389   we received from anonymous referees. We are also deeply saddened about the

  2390   %{\bf Acknowledgements:}

  2390   tragic death of our co-author, colleague and friend, Chunhan, who

  2391   %We are grateful for the comments we received from anonymous

  2391   suddenly died on 22 December 2016. He drove very much forward this work

  2392   %referees.

  2392   and extended it in his PhD-thesis with a formal verification of an

  2393   SELinux-style access control system. He was a stellar student

  2394   and very promising young researcher in the field of interactive

  2395   theorem proving. He was liked by many and indispensable for

  2396   organising the ITP'15 conference in Nanjing. Chunhan left behind a

  2397   grieving wife and eight-year-old son.