Use reflexivity in Coq proofs

[Gbury]

Currently coq proof can be quite slow (and even fail to check within reasonable time/memory).
One solution would be to change the structure of coq output from a srie of tactics to the following: write a reflexive function which would compute on a custom data structure (such as a list of resolutions).