---

Step * 2 of Lemma per-union-elim


1. [A] : Type
2. [B] : Type
3. x : per-union(A;B)
4. x ~ inl outl(x)
⊢ per-or(uand(x ~ inl outl(x);outl(x) ∈ A supposing x ~ inl outl(x));uand(x ~ inr outr(x) ;outr(x) ∈ B 
                                                                                           supposing x ~ inr outr(x) ))
BY
{ ((Assert outl(x) ∈ A BY
          (PointwiseFunctionality 3
           THEN (PerHD (-2)
                 THEN Try ((At ⌜Type⌝ UniverseIsType⋅
                            THEN RepeatFor 2 ((MemCD THEN Try (QuickAuto)))
                            THEN DUand (-1)
                            THEN RepeatFor 3 (CanonicalAuto)))⋅
                 )
           THEN DUand (-2)
           THEN RWO "-1" (-2)
           THEN Reduce (-2)
           THEN Try ((EqCD THEN Auto))
           THEN DUand (-3)
           THEN (CanonicalTestCasesHyp (-2) THENA Auto)
           THEN (D -3 THENA (DUand 0 THEN Auto))
           THEN Try (PerVoid)
           THEN Auto))
   THEN PerOrLeft⋅
   THEN (RepeatFor 2 (Try ((MemCD
                            THEN Try ((BLemma `per-union-implies-wf1` THEN Complete (Auto))⋅)
                            THEN Try ((BLemma `per-union-implies-wf2` THEN Complete (Auto))⋅))))
         THEN Try (Complete (Auto))
         THEN Try ((DUand (-2)
                    THEN Assert ⌜0 = 1 ∈ ℤ⌝⋅
                    THEN Auto
                    THEN Subst' 0 ~ 1 0
                    THEN Try (Complete (Auto))
                    THEN Assert ⌜case inr outr(x)  of inl(z) => 1 | inr(z) => 0 ~ case inl outl(x)
                                  of inl(z) =>
                                  1
                                  | inr(z) =>
                                  0⌝⋅
                    THEN Reduce (-1)
                    THEN Try (Trivial)
                    THEN EqCD
                    THEN Trivial)⋅))⋅) }

1
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))

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  outl(x)  \mmember{}  A  BY
                (PointwiseFunctionality  3
                  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)))\mcdot{}
                              )
                  THEN  DUand  (-2)
                  THEN  RWO  "-1"  (-2)
                  THEN  Reduce  (-2)
                  THEN  Try  ((EqCD  THEN  Auto))
                  THEN  DUand  (-3)
                  THEN  (CanonicalTestCasesHyp  (-2)  THENA  Auto)
                  THEN  (D  -3  THENA  (DUand  0  THEN  Auto))
                  THEN  Try  (PerVoid)
                  THEN  Auto))
  THEN  PerOrLeft\mcdot{}
  THEN  (RepeatFor  2  (Try  ((MemCD
                                                    THEN  Try  ((BLemma  `per-union-implies-wf1`  THEN  Complete  (Auto))\mcdot{})
                                                    THEN  Try  ((BLemma  `per-union-implies-wf2`  THEN  Complete  (Auto))\mcdot{}))))
              THEN  Try  (Complete  (Auto))
              THEN  Try  ((DUand  (-2)
                                    THEN  Assert  \mkleeneopen{}0  =  1\mkleeneclose{}\mcdot{}
                                    THEN  Auto
                                    THEN  Subst'  0  \msim{}  1  0
                                    THEN  Try  (Complete  (Auto))
                                    THEN  Assert  \mkleeneopen{}case  inr  outr(x)    of  inl(z)  =>  1  |  inr(z)  =>  0  \msim{}  case  inl  outl(x)
                                                                of  inl(z)  =>
                                                                1
                                                                |  inr(z)  =>
                                                                0\mkleeneclose{}\mcdot{}
                                    THEN  Reduce  (-1)
                                    THEN  Try  (Trivial)
                                    THEN  EqCD
                                    THEN  Trivial)\mcdot{}))\mcdot{})

---

Home Index