---

Step * of Lemma union-Leibniz-type

∀A,B:Type.  (Leibniz-type{i:l}(A) ⇒ Leibniz-type{i:l}(B) ⇒ Leibniz-type{i:l}(A + B))
BY
{ (Auto
   THEN All (Unfold `Leibniz-type`)
   THEN ExRepD
   THEN (D 0 With ⌜λp,q. case p
                         of inl(a) =>
                         case q of inl(a') => s1 a a' | inr(b') => True
                         | inr(b) =>
                         case q of inl(a') => True | inr(b') => sep b b'⌝ 
         THENW Auto
         )
   THEN Reduce 0
   THEN D 0
   THEN (UnivCD THENA Auto)
   THEN DVar `x'
   THEN DVar `y'
   THEN Try (DVar `z')
   THEN All Reduce
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}A,B:Type.    (Leibniz-type\{i:l\}(A)  {}\mRightarrow{}  Leibniz-type\{i:l\}(B)  {}\mRightarrow{}  Leibniz-type\{i:l\}(A  +  B))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `Leibniz-type`)
  THEN  ExRepD
  THEN  (D  0  With  \mkleeneopen{}\mlambda{}p,q.  case  p
                                              of  inl(a)  =>
                                              case  q  of  inl(a')  =>  s1  a  a'  |  inr(b')  =>  True
                                              |  inr(b)  =>
                                              case  q  of  inl(a')  =>  True  |  inr(b')  =>  sep  b  b'\mkleeneclose{} 
              THENW  Auto
              )
  THEN  Reduce  0
  THEN  D  0
  THEN  (UnivCD  THENA  Auto)
  THEN  DVar  `x'
  THEN  DVar  `y'
  THEN  Try  (DVar  `z')
  THEN  All  Reduce
  THEN  Auto)

---

Home Index