---

Step * of Lemma normal-ds-join

∀ds1,ds2:x:Id fp-> Type.  (Normal(ds1) ⇒ Normal(ds2) ⇒ Normal(ds1 ⊕ ds2))
BY
{ (((((((Auto THEN (All (RepUR ``normal-ds 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:

---

Latex:
\mforall{}ds1,ds2:x:Id  fp->  Type.    (Normal(ds1)  {}\mRightarrow{}  Normal(ds2)  {}\mRightarrow{}  Normal(ds1  \moplus{}  ds2))


By

---

Latex:
(((((((Auto  THEN  (All  (RepUR  ``normal-ds  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