Level: Lib Thy Top: 1
Hypotheses:

  1. n : {1...}

  2. E : n n

  3. EquivRel(n;i,j.i E j)

  4. x : i,j:n//(i E j)

  5. (x = n - 1)

Conclusion:

x i,j:(n - 1)//(i E j)

Applied Tactic: (InstLemma `rest_equi_rel` [n;n - 1;E] ...a)
Generated subgoals:

1. x i,j:(n - 1)//(i E j)