---

Step * of Lemma per-union-elim1

∀[A,B:Type].  ∀x:per-union(A;B). per-or(x ~ inl outl(x);x ~ inr outr(x) )
BY
{ (Auto
   THEN UseWitness ⌜if x is inl then <Ax, Ax>
                    else <0, Ax>⌝⋅
   THEN PointwiseFunctionality  (-1)
   THEN PerHD (-1)
   THEN Try ((At ⌜Type⌝ UniverseIsType⋅
              THEN RepeatFor 2 ((MemCD THEN Try (QuickAuto)))
              THEN DUand (-1)
              THEN RepeatFor 3 (CanonicalAuto)))
   THEN Repeat (All DUand )
   THEN MoveToConcl (-1)
   THEN Repeat ((CanonicalTestCases THENA CompleteAuto
                 THEN Try (((D 0 THENA Auto) THEN (D -1 THENA (DUand 0 THEN Complete (Auto))) THEN Try (PerVoid)))
                 THEN Try ((BLemma `member-per-or-left` THEN Auto THEN CanonicalAuto)⋅)))
   THEN Try ((BLemma `member-per-or-right` THEN Auto THEN CanonicalAuto)⋅)
   THEN EqCDA
   THEN Try ((BLemma `member-per-or-right` THEN Auto THEN CanonicalAuto)⋅)
   THEN Try ((BLemma `member-per-or-left` THEN Auto THEN CanonicalAuto)⋅)
   THEN (BLemma `per-or-equal` THENW Auto)
   THEN (RepeatFor 2 (D 0) THENA Auto)
   THEN D -1
   THEN Auto
   THEN ApFunSq `Z' ⌜case Z of inl(_) => 0 | inr(_) => 1⌝ (-1)⋅
   THEN Assert ⌜0 = 1 ∈ ℤ⌝⋅
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  UseWitness  \mkleeneopen{}if  x  is  inl  then  <Ax,  Ax>
                                    else  ɘ,  Ax>\mkleeneclose{}\mcdot{}
  THEN  PointwiseFunctionality    (-1)
  THEN  PerHD  (-1)
  THEN  Try  ((At  \mkleeneopen{}Type\mkleeneclose{}  UniverseIsType\mcdot{}
                        THEN  RepeatFor  2  ((MemCD  THEN  Try  (QuickAuto)))
                        THEN  DUand  (-1)
                        THEN  RepeatFor  3  (CanonicalAuto)))
  THEN  Repeat  (All  DUand  )
  THEN  MoveToConcl  (-1)
  THEN  Repeat  ((CanonicalTestCases  THENA  CompleteAuto
                              THEN  Try  (((D  0  THENA  Auto)
                                                    THEN  (D  -1  THENA  (DUand  0  THEN  Complete  (Auto)))
                                                    THEN  Try  (PerVoid)))
                              THEN  Try  ((BLemma  `member-per-or-left`  THEN  Auto  THEN  CanonicalAuto)\mcdot{})))
  THEN  Try  ((BLemma  `member-per-or-right`  THEN  Auto  THEN  CanonicalAuto)\mcdot{})
  THEN  EqCDA
  THEN  Try  ((BLemma  `member-per-or-right`  THEN  Auto  THEN  CanonicalAuto)\mcdot{})
  THEN  Try  ((BLemma  `member-per-or-left`  THEN  Auto  THEN  CanonicalAuto)\mcdot{})
  THEN  (BLemma  `per-or-equal`  THENW  Auto)
  THEN  (RepeatFor  2  (D  0)  THENA  Auto)
  THEN  D  -1
  THEN  Auto
  THEN  ApFunSq  `Z'  \mkleeneopen{}case  Z  of  inl($_{}$)  =>  0  |  inr($_{}$)  =>\000C  1\mkleeneclose{}  (-1)\mcdot{}
  THEN  Assert  \mkleeneopen{}0  =  1\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index