Van Baalen, I. & Matsijs, G. M.: Coq proof of van Baalen's _diallelus_ model

A formal proof in Coq of Van Baalen's model for the possibility of knowledge of the external world despite the diallelus.