Clean
Add Coq formalization of theorem 1 with Explicit Semantic encoding