---

Step * 1 1 of Lemma per-union-elim


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)
BY
{ ((Assert per-function(per-value();a.Type) ∈ 𝕌' BY
          (BLemma `per-function_wf_type` THEN Auto))
   THEN (DupHyp (-1) THEN Unfold `per-function` -1)
   THEN (PointwiseFunctionalityForEquality' 3 THENW Auto)
   THEN ((Unfold `per-function` 0 THEN PerEqCD_member) THENW Auto)
   THEN Reduce 0
   THEN D 0
   THEN Reduce 0
   THEN Auto) }

1
1. A : Type
2. B : Type
3. x : Base
4. x1 : Base
5. x = x1 ∈ per-union(A;B)
6. per-function(per-value();a.Type) ∈ 𝕌'
7. pertype(λf,g. function-eq(per-value();a.Type;f;g)) ∈ 𝕌'
8. a : Base
9. b : Base
10. a = b ∈ per-value()
⊢ if a = Ax then x ~ inl outl(x) otherwise x ~ inr outr(x) 
= if b = Ax then x1 ~ inl outl(x1) otherwise x1 ~ inr outr(x1) 
∈ Type

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  x  :  per-union(A;B)
\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:
((Assert  per-function(per-value();a.Type)  \mmember{}  \mBbbU{}'  BY
                (BLemma  `per-function\_wf\_type`  THEN  Auto))
  THEN  (DupHyp  (-1)  THEN  Unfold  `per-function`  -1)
  THEN  (PointwiseFunctionalityForEquality'  3  THENW  Auto)
  THEN  ((Unfold  `per-function`  0  THEN  PerEqCD\_member)  THENW  Auto)
  THEN  Reduce  0
  THEN  D  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index