Level: Lib Thy Top: 1 2
Hypotheses:

  1. A :

  2. B :

  3. f : A B

  4. R : B B

  5. a:B. a R a

  6. a,b:B. a R b b R a

  7. a,b,c:B. a R b b R c a R c

  8. a : A

  9. b : A

  10. (f a) R (f b)

Conclusion:

(f b) R (f a)

Applied Tactic: (BHyp 6 ...)
Generated subgoals:

None