Level: Lib Thy Top: 1 1
Hypotheses:

  1. n : {1...}

  2. m : n

  3. E : n n

  4. Refl(n;x,y.x E y)

  5. Sym(n;x,y.x E y)

  6. Trans(n;x,y.x E y)

Conclusion:

Refl(m;x,y.x E y) Sym(m;x,y.x E y) Trans(m;x,y.x E y)

Applied Tactic: (D 0 ...a)
Generated subgoals:

1. Refl(m;x,y.x E y)

2. Sym(m;x,y.x E y) Trans(m;x,y.x E y)