---

Step * 2 1 of Lemma per-union-elim


1. [A] : Type
2. [B] : Type
3. x : per-union(A;B)
4. x ~ inl outl(x)
5. outl(x) ∈ A
⊢ uand(x ~ inl outl(x);outl(x) ∈ A supposing x ~ inl outl(x))
BY
{ ((DUand 0 THEN Try (Complete (Auto)))
   THEN (InstLemma `per-union-implies-wf1` [⌜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{}  inl  outl(x)
5.  outl(x)  \mmember{}  A
\mvdash{}  uand(x  \msim{}  inl  outl(x);outl(x)  \mmember{}  A  supposing  x  \msim{}  inl  outl(x))


By

---

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

---

Home Index