Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
A:
.
L:L(A). Refl(A List;x,y.x Rl y)
Applied Tactic:
(UnivCD ...a)
Generated subgoals:
1
. Refl(A List;x,y.x Rl y)
A:
. L:L(A). Refl(A List;x,y.x Rl y)