Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
. {T=
}
{T
}
Applied Tactic:
Unfold `subtype` 0 THEN Auto
Generated subgoals:
1
. x
{T
}
T:
. {T=
} 
{T
}
{T}