---

Step * 2 of Lemma per-union_wf


1. A : Type
2. B : Type
3. x : Base
4. y : Base
5. (x)↓
6. (y)↓
7. if x is inl then if y is inl then outl(x) = outl(y) ∈ A
                    else per-void()
   else if x is inr then if y is inr then outr(x) = outr(y) ∈ B
                         else per-void()
        else per-void() 
   supposing uand((x)↓;(y)↓)
8. uand((y)↓;(x)↓)
⊢ Ax ∈ if y is inl then if x is inl then outl(y) = outl(x) ∈ A
                        else per-void()
       else if y is inr then if x is inr then outr(y) = outr(x) ∈ B
                             else per-void()
            else per-void()
BY
{ (Thin (-1)
   THEN MoveToConcl (-1)
   THEN Repeat ((CanonicalTestCases⋅ THENA Auto))
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN Auto
   THEN Try (PerVoid)
   THEN DUand 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  x  :  Base
4.  y  :  Base
5.  (x)\mdownarrow{}
6.  (y)\mdownarrow{}
7.  if  x  is  inl  then  if  y  is  inl  then  outl(x)  =  outl(y)
                                        else  per-void()
      else  if  x  is  inr  then  if  y  is  inr  then  outr(x)  =  outr(y)
                                                  else  per-void()
                else  per-void() 
      supposing  uand((x)\mdownarrow{};(y)\mdownarrow{})
8.  uand((y)\mdownarrow{};(x)\mdownarrow{})
\mvdash{}  Ax  \mmember{}  if  y  is  inl  then  if  x  is  inl  then  outl(y)  =  outl(x)
                                                else  per-void()
              else  if  y  is  inr  then  if  x  is  inr  then  outr(y)  =  outr(x)
                                                          else  per-void()
                        else  per-void()


By

---

Latex:
(Thin  (-1)
  THEN  MoveToConcl  (-1)
  THEN  Repeat  ((CanonicalTestCases\mcdot{}  THENA  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  Auto
  THEN  Try  (PerVoid)
  THEN  DUand  0
  THEN  Auto)

---

Home Index