Level: Lib Thy Top:
Hypotheses:None
Conclusion:
E:
EquivRel(;x,y.x E y) 
(x,y:. Dec(x E y))
(
h: . (n,k:. n E k 
h n = h k) (n:. n E (h n)))
Applied Tactic: UnivCD THENW Auto THEN D 2
Generated subgoals:1. h: . (n,k:. n E k h n = h k) (n:. n E (h n))