---

Step * 1 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. 0 ≤ 0
7. (b)↓
8. per-void() supposing uand(0 ≤ 0;(b)↓)
9. a ~ inl outl(a)
10. ∀[u,v:Top].  (if b is inl then u else v ~ v)
⊢ b = (inl outl(b)) ∈ Base
BY
{ (D (-3) 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.  0  \mleq{}  0
7.  (b)\mdownarrow{}
8.  per-void()  supposing  uand(0  \mleq{}  0;(b)\mdownarrow{})
9.  a  \msim{}  inl  outl(a)
10.  \mforall{}[u,v:Top].    (if  b  is  inl  then  u  else  v  \msim{}  v)
\mvdash{}  b  =  (inl  outl(b))


By

---

Latex:
(D  (-3)  THEN  Try  (PerVoid)  THEN  DUand  0  THEN  Auto)

---

Home Index