---

Step * 1 of Lemma per-union_wf


1. A : Type
2. B : Type
3. x : Base
4. y : Base
5. (x)↓
6. (y)↓
⊢ 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() ∈ Type
BY
{ (Repeat ((CanonicalTestCases⋅ THENA Auto)) THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  x  :  Base
4.  y  :  Base
5.  (x)\mdownarrow{}
6.  (y)\mdownarrow{}
\mvdash{}  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()  \mmember{}  Type


By

---

Latex:
(Repeat  ((CanonicalTestCases\mcdot{}  THENA  Auto))  THEN  Auto)

---

Home Index