Level:
Lib
Thy
Top
:
2
Hypotheses:
n : {1...}
E :
n
n
EquivRel(
n;i,j.i E j)
x : i,j:
n//(i E j)
Conclusion:
n - 1
i,j:
n//(i E j)
Applied Tactic:
(InstLemma `incl_aux1_quo` [
n
;
E
;
n - 1
] ...)
Generated subgoals:
None
n 
n 
n;i,j.i E j)n//(i E j)
n - 1 
i,j:n//(i E j)
n
;E;n - 1] ...)