Level: Lib Thy Top: 1
Hypotheses:

  1. A :

  2. B :

  3. f : A B

  4. R : B B

  5. Bij(A;B;f)

  6. EquivRel(B;x,y.x R y)

Conclusion:

F:x,y:A//(x R_f y) x,y:B//(x R y). Bij(x,y:A//(x R_f y);x,y:B//(x R y);F)

Applied Tactic: (InstLemma `preima_of_equiv_rel` [A;B;f;R] ...a)
Generated subgoals:

1. F:x,y:A//(x R_f y) x,y:B//(x R y). Bij(x,y:A//(x R_f y);x,y:B//(x R y);F)