---

Step * of Lemma product-union-atom-disjoint

∀[T,S,A,B:Type].  (¬T × S ⋂ (A + B) ⋃ Atom)
BY
{ (Auto
   THEN (D 0 THEN Auto)
   THEN RenameVar `x' (-1)
   THEN Isect2HD (-1)
   THEN (Assert ↑ispair(x) BY
               (RW (AddrC [1;1] (LemmaC `pair-eta`)) 0 THEN Reduce 0 THEN Auto))⋅
   THEN MoveToConcl (-1)
   THEN GenConcl ⌜x = z ∈ ((A + B) ⋃ Atom)⌝⋅
   THEN Auto
   THEN OnSomeHyp D_b_union
   THEN Try (Complete ((DProdsAndUnions THEN AllReduce THEN Auto)))
   THEN Try ((CanonicalTestCases THEN Auto THEN Fold `has-value` 0 THEN Auto))
   THEN MoveToConcl (-1)
   THEN Fold `not` 0
   THEN BLemma `isatom-implies-not-ispair`
   THEN Auto
   THEN Try (ProveHasValue)
   THEN (Subst ⌜isatom(a1) ~ tt⌝ 0⋅ THENM Auto)
   THEN IsatomReduceTrue
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,S,A,B:Type].    (\mneg{}T  \mtimes{}  S  \mcap{}  (A  +  B)  \mcup{}  Atom)


By

---

Latex:
(Auto
  THEN  (D  0  THEN  Auto)
  THEN  RenameVar  `x'  (-1)
  THEN  Isect2HD  (-1)
  THEN  (Assert  \muparrow{}ispair(x)  BY
                          (RW  (AddrC  [1;1]  (LemmaC  `pair-eta`))  0  THEN  Reduce  0  THEN  Auto))\mcdot{}
  THEN  MoveToConcl  (-1)
  THEN  GenConcl  \mkleeneopen{}x  =  z\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  OnSomeHyp  D\_b\_union
  THEN  Try  (Complete  ((DProdsAndUnions  THEN  AllReduce  THEN  Auto)))
  THEN  Try  ((CanonicalTestCases  THEN  Auto  THEN  Fold  `has-value`  0  THEN  Auto))
  THEN  MoveToConcl  (-1)
  THEN  Fold  `not`  0
  THEN  BLemma  `isatom-implies-not-ispair`
  THEN  Auto
  THEN  Try  (ProveHasValue)
  THEN  (Subst  \mkleeneopen{}isatom(a1)  \msim{}  tt\mkleeneclose{}  0\mcdot{}  THENM  Auto)
  THEN  IsatomReduceTrue
  THEN  Auto)

---

Home Index