---

Step * of Lemma member-per-product

∀[A:Type]. ∀[B:per-function(A;a.Type)]. ∀[a:A]. ∀[b:B[a]].  (<a, b> ∈ per-product(A;a.B[a]))
BY
{ (TACTIC:Intro
   THEN (InstLemma `per-function_wf_type` [⌜A⌝]⋅ THENA Auto)
   THEN Intro
   THEN At ⌜Type⌝Intros⋅
   THEN Unhide
   THEN (Assert per-product(A;a.B[a]) ∈ Type BY
               (InstLemma `per-product_wf` [⌜A⌝;⌜B⌝]⋅ THEN Auto))
   THEN Thin 2) }

1
1. A : Type
2. B : per-function(A;a.Type)
3. a : A
4. b : B[a]
5. per-product(A;a.B[a]) ∈ Type
⊢ <a, b> ∈ per-product(A;a.B[a])

---

Latex:

---

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


By

---

Latex:
(TACTIC:Intro
  THEN  (InstLemma  `per-function\_wf\_type`  [\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Intro
  THEN  At  \mkleeneopen{}Type\mkleeneclose{}Intros\mcdot{}
  THEN  Unhide
  THEN  (Assert  per-product(A;a.B[a])  \mmember{}  Type  BY
                          (InstLemma  `per-product\_wf`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  Thin  2)

---

Home Index