Provide reference material for the .fq format

[facundominguez]

While LH continues to interface with LF using the Fixpoint.FInfo type, people debugging LH will need to understand .fq files which are the textual representation of FInfo.

The README provides some hints, but it would need to go into more details. For instance,

• the sort representation
• the meaning of bindings (and duplicated bindings) in constraint environments
• the invariants on the numbering of bindings
• the meaning of match clauses
• the predicate qualifiers
• the liquid variables
• ... and all the other declarations