---

Step * of Lemma per-union-implies-wf2

∀[A,B:Type]. ∀[x:per-union(A;B)].  (x ~ inr outr(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 ((At ⌜Type⌝ UniverseIsType⋅
                    THEN RepeatFor 2 ((MemCD THEN Try (QuickAuto)))
                    THEN DUand (-1)
                    THEN RepeatFor 3 (CanonicalAuto)))
         )
   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 ((D (-3) THEN Try (PerVoid) THEN DUand 0 THEN Auto)⋅)) }

1
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

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[x:per-union(A;B)].    (x  \msim{}  inr  outr(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  ((At  \mkleeneopen{}Type\mkleeneclose{}  UniverseIsType\mcdot{}
                                    THEN  RepeatFor  2  ((MemCD  THEN  Try  (QuickAuto)))
                                    THEN  DUand  (-1)
                                    THEN  RepeatFor  3  (CanonicalAuto)))
              )
  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  ((D  (-3)  THEN  Try  (PerVoid)  THEN  DUand  0  THEN  Auto)\mcdot{}))

---

Home Index