Level: Lib Thy Top: 1 3
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. c : A

  11. (f a) R (f b)

  12. (f b) R (f c)

Conclusion:

(f a) R (f c)

Applied Tactic: (FHyp 7 [11;12] ...)
Generated subgoals:

None