---

Step * of Lemma hdf-sqequal9

∀[mk-hdf,a,s:Top].
  (let b ←─ a
   in case null(b) of inl(x1) => let s' ←─ s in <mk-hdf s', s'> | inr(y1) => <mk-hdf b, b> ~ let b ←─ a
                                                                              in let s' ←─ case null(b)
                                                                                  of inl(x1) =>
                                                                                  s
                                                                                  | inr(y1) =>
                                                                                  b
                                                                                 in <mk-hdf s', s'>)
BY
{ ((UnivCD THENA Auto) THEN SymbComp 0 THEN LiftRed THEN Auto) }

---

Latex:


\mforall{}[mk-hdf,a,s:Top].
    (let  b  \mleftarrow{}{}  a
      in  case  null(b)  of  inl(x1)  =>  let  s'  \mleftarrow{}{}  s  in  <mk-hdf  s',  s'>  |  inr(y1)  =>  <mk-hdf  b,  b>  \msim{}  let  b  \mleftarrow{}\000C{}  a
                                                                                                                                                            in  let  s'  \mleftarrow{}{}
                                                                                                                                                                    case  null(b)
                                                                                                                                                                    of  inl(x1)  =>
                                                                                                                                                                    s
                                                                                                                                                                    |  inr(y1)  =>
                                                                                                                                                                    b
                                                                                                                                                                  in  <mk-hdf  s',  s'>)


By

((UnivCD  THENA  Auto)  THEN  SymbComp  0  THEN  LiftRed  THEN  Auto)

---

Home Index