Unify and proofs

* insert unify function
* insert same rule
* insert new example proof