---

Step * 3 1 of Lemma per-union-elim


1. [A] : Type
2. [B] : Type
3. x : per-union(A;B)
4. x ~ inr outr(x) 
5. outr(x) ∈ B
⊢ uand(x ~ inr outr(x) ;outr(x) ∈ B supposing x ~ inr outr(x) )
BY
{ ((DUand 0 THEN Try (Complete (Auto)))
   THEN (InstLemma `per-union-implies-wf2` [⌜A⌝;⌜B⌝;⌜x⌝]⋅ THENA Auto)
   THEN (Unfold `uimplies` 0 THEN MemCD)⋅
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  x  :  per-union(A;B)
4.  x  \msim{}  inr  outr(x) 
5.  outr(x)  \mmember{}  B
\mvdash{}  uand(x  \msim{}  inr  outr(x)  ;outr(x)  \mmember{}  B  supposing  x  \msim{}  inr  outr(x)  )


By

---

Latex:
((DUand  0  THEN  Try  (Complete  (Auto)))
  THEN  (InstLemma  `per-union-implies-wf2`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Unfold  `uimplies`  0  THEN  MemCD)\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index