---

Step * 1 of Lemma per-union-elim

.....aux..... 
1. A : Type
2. B : Type
3. x : per-union(A;B)
4. per-product(per-value();x@0.if x@0 = Ax then x ~ inl outl(x) otherwise x ~ inr outr(x) )
⊢ λx@0.if x@0 = Ax then x ~ inl outl(x) otherwise x ~ inr outr(x)  ∈ per-function(per-value();a.Type)
BY
{ All Thin }

1
1. A : Type
2. B : Type
3. x : per-union(A;B)
⊢ λx@0.if x@0 = Ax then x ~ inl outl(x) otherwise x ~ inr outr(x)  ∈ per-function(per-value();a.Type)

---

Latex:

---

Latex:
.....aux..... 
1.  A  :  Type
2.  B  :  Type
3.  x  :  per-union(A;B)
4.  per-product(per-value();x@0.if  x@0  =  Ax  then  x  \msim{}  inl  outl(x)  otherwise  x  \msim{}  inr  outr(x)  )
\mvdash{}  \mlambda{}x@0.if  x@0  =  Ax  then  x  \msim{}  inl  outl(x)  otherwise  x  \msim{}  inr  outr(x) 
    \mmember{}  per-function(per-value();a.Type)


By

---

Latex:
All  Thin

---

Home Index