---

Step * 1 1 1 of Lemma per-union-elim


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
BY
{ ((Assert a = b ∈ Base BY
          (SubsumeC ⌜per-value()⌝⋅ THEN Auto))
   THEN HypSubst' (-1) 0
   THEN (GenConcl ⌜b = z ∈ per-value()⌝⋅ THENA Auto)
   THEN (InstLemma `per-value-property` [⌜z⌝]⋅ THENA Auto)
   THEN DUand (-1)
   THEN CanonicalAuto) }

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()
11. a = b ∈ Base
12. z : per-value()
13. b = z ∈ per-value()
14. z ∈ Base
15. (z)↓
16. x2 : z ~ Ax
⊢ (x ~ inl outl(x)) = (x1 ~ inl outl(x1)) ∈ Type

2
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()
11. a = b ∈ Base
12. z : per-value()
13. b = z ∈ per-value()
14. z ∈ Base
15. (z)↓
16. ∀[u,v:Top].  (if z = Ax then u otherwise v ~ v)
⊢ (x ~ inr outr(x) ) = (x1 ~ inr outr(x1) ) ∈ Type

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  x  :  Base
4.  x1  :  Base
5.  x  =  x1
6.  per-function(per-value();a.Type)  \mmember{}  \mBbbU{}'
7.  pertype(\mlambda{}f,g.  function-eq(per-value();a.Type;f;g))  \mmember{}  \mBbbU{}'
8.  a  :  Base
9.  b  :  Base
10.  a  =  b
\mvdash{}  if  a  =  Ax  then  x  \msim{}  inl  outl(x)  otherwise  x  \msim{}  inr  outr(x) 
=  if  b  =  Ax  then  x1  \msim{}  inl  outl(x1)  otherwise  x1  \msim{}  inr  outr(x1) 


By

---

Latex:
((Assert  a  =  b  BY
                (SubsumeC  \mkleeneopen{}per-value()\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  HypSubst'  (-1)  0
  THEN  (GenConcl  \mkleeneopen{}b  =  z\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `per-value-property`  [\mkleeneopen{}z\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  DUand  (-1)
  THEN  CanonicalAuto)

---

Home Index