Saturate negative conversion rules with inversions

[ppedrot]

We dive into paranoïa for the side-conditions of η-rules for functions and pairs. That is, we saturate the isWfFun and isWfPair with everything we have at hand about the considered subterms. This is done by semantizing the corresponding predicates in the logical relation, introducing the semantic counterparts isLRFun and isLRPair.

• Functions could even be a tad more paranoid (asking for inversions on the codomain type) but it would require more work and it's already better now.
• Some self-convertibility hypotheses in prod / sigma term reducibility are probably redundant now since the semantic predicates imply them once we have escape, I didn't look into that.