Theorem: HTPI.elt_Univ (HTPILib/Chap8Part2.lean)

State before:
U : Type
u : U
⊢ u ∈ Univ U
Tactic:
trivial
State after:
no goals