---

Step * of Lemma member-per-or-left

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

1
.....wf..... 
1. A : Type
2. B : Type
3. a : A
⊢ λx.if x = Ax then A otherwise B ∈ per-function(per-value();a.Type)

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

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[a:A].    (<Ax,  a>  \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))

---

Home Index