---

Step * 1 of Lemma per-union-implies-wf2


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 outr(a) = outr(b) ∈ B else per-void() supposing uand((a)↓;0 ≤ 0)
9. b ~ inr outr(b) 
10. ∀[u,v:Top].  (if a is inl then u else v ~ v)
⊢ a = (inr outr(a) ) ∈ Base
BY
{ (CanonicalTestCasesHyp (-3)
   THEN Auto
   THEN (Try ((RWO "-1<" 0 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  outr(a)  =  outr(b)  else  per-void()  supposing  uand((a)\mdownarrow{};0  \mleq{}  0)
9.  b  \msim{}  inr  outr(b) 
10.  \mforall{}[u,v:Top].    (if  a  is  inl  then  u  else  v  \msim{}  v)
\mvdash{}  a  =  (inr  outr(a)  )


By

---

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

---

Home Index