---

Step * of Lemma hdf-sqequal8-2

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

---

Latex:


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


By

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

---

Home Index