---

Step * of Lemma per-union-implies-wf1

∀[A,B:Type]. ∀[x:per-union(A;B)].  (x ~ inl outl(x) ∈ ℙ)
BY
{ (Intros
   THEN Unhide
   THEN PointwiseFunctionality (-1)
   THEN Auto
   THEN EqCD
   THEN Auto
   THEN Unfold `prop` 0
   THEN Refine_sqequalExtensionalEquality
   THEN D 0
   THEN Auto
   THEN PerHD (-2)
   THEN Try ((RWO "-1" (-2)
              THEN Reduce (-2)
              THEN ∀h:hyp. Repeat (DUand h) 
              THEN CanonicalTestCasesHyp (-2)
              THEN Auto
              THEN Try ((RWO "-1<" 0 THEN Auto))⋅))
   THEN Try ((At ⌜Type⌝ UniverseIsType⋅
              THEN RepeatFor 2 ((MemCD THEN Try (QuickAuto)))
              THEN DUand (-1)
              THEN RepeatFor 3 (CanonicalAuto)))) }

1
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

2
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

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[x:per-union(A;B)].    (x  \msim{}  inl  outl(x)  \mmember{}  \mBbbP{})


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  PointwiseFunctionality  (-1)
  THEN  Auto
  THEN  EqCD
  THEN  Auto
  THEN  Unfold  `prop`  0
  THEN  Refine\_sqequalExtensionalEquality
  THEN  D  0
  THEN  Auto
  THEN  PerHD  (-2)
  THEN  Try  ((RWO  "-1"  (-2)
                        THEN  Reduce  (-2)
                        THEN  \mforall{}h:hyp.  Repeat  (DUand  h) 
                        THEN  CanonicalTestCasesHyp  (-2)
                        THEN  Auto
                        THEN  Try  ((RWO  "-1<"  0  THEN  Auto))\mcdot{}))
  THEN  Try  ((At  \mkleeneopen{}Type\mkleeneclose{}  UniverseIsType\mcdot{}
                        THEN  RepeatFor  2  ((MemCD  THEN  Try  (QuickAuto)))
                        THEN  DUand  (-1)
                        THEN  RepeatFor  3  (CanonicalAuto))))

---

Home Index