Refactor all code into Coq

[mekty2012]

The operational semantics visualized here would not reflect well concepts from nondeterminism, and also some features for lambda calculus.

Refactor all code into small step operational semantics given as Inductive Proposition. For details, see programming language foundation in software foundation series.

Also, my goal is to prove that denotational semantics given coincide with operational semantics. Therefore, it may be helpful to have category theory implementation in Coq as library.

[mekty2012]

Specification

1. Implement domain theory. Done. Some proof required.
2. If required, implement category theory related theorems. This repository will be helpful.
3. Also, adding input&output will makes it harder to create 'good' domain. If required, use coinductive type with follwoing references.
   http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/bertot_sl2.pdf
   https://www.labri.fr/perso/casteran/CoqArt/Tsinghua/C7.pdf Done.