Kalmar Agda proof for the completeness of propositional logic using Kalmar's lemma. The completeness theorem is in the end of "Kalmar.agda". We use the Agda version 2.6.2, and Agda stdlib verion 2.0.