---

Step * of Lemma per-union_wf

∀[A,B:Type].  (per-union(A;B) ∈ Type)
BY
{ TACTIC:(Auto THEN PerEqCD THEN Auto THEN Repeat (All DUand) THEN Auto) }

1
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

2
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()

3
1. A : Type
2. B : Type
3. x : Base
4. y : Base
5. z : Base
6. (x)↓
7. (y)↓
8. 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)↓)
9. (y)↓
10. (z)↓
11. if y is inl then if z is inl then outl(y) = outl(z) ∈ A
                     else per-void()
    else if y is inr then if z is inr then outr(y) = outr(z) ∈ B
                          else per-void()
         else per-void() 
    supposing uand((y)↓;(z)↓)
12. uand((x)↓;(z)↓)
⊢ Ax ∈ if x is inl then if z is inl then outl(x) = outl(z) ∈ A
                        else per-void()
       else if x is inr then if z is inr then outr(x) = outr(z) ∈ B
                             else per-void()
            else per-void()

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    (per-union(A;B)  \mmember{}  Type)


By

---

Latex:
TACTIC:(Auto  THEN  PerEqCD  THEN  Auto  THEN  Repeat  (All  DUand)  THEN  Auto)

---

Home Index