DEFINITION iso_refl()
TYPE =
       ∀t:T.(iso t t)
BODY =
Show proof