---

Step * of Lemma member-per-union-right

∀[A,B:Type]. ∀[x:B].  (inr x  ∈ per-union(A;B))
BY
{ (Auto
   THEN RepUR ``per-union`` 0
   THEN UnfoldTopAb 0
   THEN At ⌜Type⌝ (PointwiseFunctionality (-1))⋅
   THEN Try ((EqCD THEN Try (Trivial) THEN Try ((Fold `per-union` 0 THEN Fold `member` 0 THEN Auto))))
   THEN Try ((Refine_pertypeMemberEquality ⌜A⌝⋅
              THEN Try ((Fold `per-union` 0 THEN Auto))
              THEN Reduce 0
              THEN Repeat (DUand 0)
              THEN Reduce 0
              THEN Auto
              THEN CanonicalAuto))) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RepUR  ``per-union``  0
  THEN  UnfoldTopAb  0
  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  (PointwiseFunctionality  (-1))\mcdot{}
  THEN  Try  ((EqCD  THEN  Try  (Trivial)  THEN  Try  ((Fold  `per-union`  0  THEN  Fold  `member`  0  THEN  Auto))))
  THEN  Try  ((Refine\_pertypeMemberEquality  \mkleeneopen{}A\mkleeneclose{}\mcdot{}
                        THEN  Try  ((Fold  `per-union`  0  THEN  Auto))
                        THEN  Reduce  0
                        THEN  Repeat  (DUand  0)
                        THEN  Reduce  0
                        THEN  Auto
                        THEN  CanonicalAuto)))

---

Home Index