Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
eq:{T
}.
u:T.
(eq u u)
Applied Tactic:
D 0 THENA Auto THEN D 0 THENA Auto
Generated subgoals:
1
.
u:T.
(eq u u)
T:
. eq:{T
}. u:T. 
(eq u u)u:T. (eq u u)