---

Step * of Lemma normal-da-join

∀[da1,da2:x:Knd fp-> Type].  (Normal(da1 ⊕ da2)) supposing (Normal(da2) and Normal(da1))
BY
{ (((((((Auto THEN (All (RepUR ``normal-da fpf-all``)) THEN Auto THEN RWO "fpf-join-ap-sq" 0) THENA Auto)
       THEN (RWO "fpf-join-dom" (-1))
       )
      THENA Auto
      )
     THEN SplitOnConclITE
     )
    THENA Auto
    )
   THEN BackThruSomeHyp
   THEN Auto
   THEN SplitOrHyps
   THEN Auto) }

---

Latex:


\mforall{}[da1,da2:x:Knd  fp->  Type].    (Normal(da1  \moplus{}  da2))  supposing  (Normal(da2)  and  Normal(da1))


By

(((((((Auto  THEN  (All  (RepUR  ``normal-da  fpf-all``))  THEN  Auto  THEN  RWO  "fpf-join-ap-sq"  0)
            THENA  Auto
            )
          THEN  (RWO  "fpf-join-dom"  (-1))
          )
        THENA  Auto
        )
      THEN  SplitOnConclITE
      )
    THENA  Auto
    )
  THEN  BackThruSomeHyp
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto)

---

Home Index