---

Step * of Lemma member-per-or-right

∀[A,B:Type]. ∀[b:B].  (<0, b> ∈ per-or(A;B))
BY
{ TACTIC:(Auto
          THEN Unfold `per-or` 0
          THEN Unfold `per-exists` 0
          THEN (BLemma `member-per-product` THENA Auto)
          THEN Try ((Fold `per-or-family` 0 THEN Auto))) }

1
.....wf..... 
1. A : Type
2. B : Type
3. b : B
⊢ 0 ∈ per-value()

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[b:B].    (ɘ,  b>  \mmember{}  per-or(A;B))


By

---

Latex:
TACTIC:(Auto
                THEN  Unfold  `per-or`  0
                THEN  Unfold  `per-exists`  0
                THEN  (BLemma  `member-per-product`  THENA  Auto)
                THEN  Try  ((Fold  `per-or-family`  0  THEN  Auto)))

---

Home Index