---

Step * 2 of Lemma per-union-implies-wf1


1. A : Type
2. B : Type
3. a : Base
4. b : Base
5. c : a = b ∈ per-union(A;B)
6. (a)↓
7. 0 ≤ 0
8. if a is inr then per-void() else per-void() supposing uand((a)↓;0 ≤ 0)
9. b ~ inl outl(b)
10. ∀[u,v:Top].  (if a is inl then u else v ~ v)
⊢ a = (inl outl(a)) ∈ Base
BY
{ (CanonicalTestCasesHyp (-3)⋅ THEN Auto THEN (D (-4) THEN Try (PerVoid) THEN DUand 0 THEN Auto)⋅)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  a  :  Base
4.  b  :  Base
5.  c  :  a  =  b
6.  (a)\mdownarrow{}
7.  0  \mleq{}  0
8.  if  a  is  inr  then  per-void()  else  per-void()  supposing  uand((a)\mdownarrow{};0  \mleq{}  0)
9.  b  \msim{}  inl  outl(b)
10.  \mforall{}[u,v:Top].    (if  a  is  inl  then  u  else  v  \msim{}  v)
\mvdash{}  a  =  (inl  outl(a))


By

---

Latex:
(CanonicalTestCasesHyp  (-3)\mcdot{}  THEN  Auto  THEN  (D  (-4)  THEN  Try  (PerVoid)  THEN  DUand  0  THEN  Auto)\mcdot{})\mcdot{}

---

Home Index