---

Step * of Lemma hdf-sqequal8-3

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

---

Latex:

---

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


By

---

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

---

Home Index