Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

A,B:. f:A B. R:B B . R_f A A

Applied Tactic: (UnivCD THENM Unfold `preima_of_rel` 0 ...)
Generated subgoals:

None