---

Step * of Lemma member-per-and

∀[A:Type]. ∀[B:Type supposing A]. ∀[a:A]. ∀[b:B].  (<a, b> ∈ per-and(A;B))
BY
{ TACTIC:(Intros
          THEN (Assert B ∈ Type BY
                      Auto)
          THEN Auto
          THEN Unfold `per-and` 0⋅
          THEN InstLemma `member-per-product` [⌜A⌝;⌜λ2u.B⌝]⋅
          THEN Auto) }

1
.....wf..... 
1. A : Type
2. B : ⋂:A. Type
3. a : A
4. B ∈ Type
5. b : B
6. Type
⊢ λu.B ∈ per-function(A;a.Type)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:Type  supposing  A].  \mforall{}[a:A].  \mforall{}[b:B].    (<a,  b>  \mmember{}  per-and(A;B))


By

---

Latex:
TACTIC:(Intros
                THEN  (Assert  B  \mmember{}  Type  BY
                                        Auto)
                THEN  Auto
                THEN  Unfold  `per-and`  0\mcdot{}
                THEN  InstLemma  `member-per-product`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}u.B\mkleeneclose{}]\mcdot{}
                THEN  Auto)

---

Home Index