Level: Lib Thy Top:
Hypotheses:None
Conclusion:
n:{1...}. m:
n. E:n 
n 
. EquivRel(n;x,y.x E y) 
EquivRel(m;x,y.x E y)
Applied Tactic: (UnivCD THENM Unfold `equiv_rel` 0 ...a)
Generated subgoals:1. Refl(m;x,y.x E y) 
Sym(m;x,y.x E y) Trans(m;x,y.x E y)