Step
*
of Lemma
hdf_ap_halt_lemma
∀x:Top. (hdf-halt()(x) ~ <hdf-halt(), {}>)
BY
{ (UnivCD THENA Auto) }
1
1. x : Top@i
⊢ hdf-halt()(x) ~ <hdf-halt(), {}>
Latex:
Latex:
\mforall{}x:Top.  (hdf-halt()(x)  \msim{}  <hdf-halt(),  \{\}>)
By
Latex:
(UnivCD  THENA  Auto)
Home
Index