uniqueness-type-proofs

This is the formalization of an uniqueness type system in a Java-like imperitive language. It's layered in two fold.

• The Proof holds the proof over a language without subtyping feature.
• The Proof_subtype holds the proof over a language with subtyping/subclassing relation.