---

Step * of Lemma per-product-elim

∀[A:Type]. ∀[B:per-function(A;a.Type)]. ∀[p:per-product(A;a.B[a])].
  uand(p ~ <fst(p), snd(p)>;uand(fst(p) ∈ A;snd(p) ∈ B[fst(p)]))
BY
{ (Intro
   THEN (InstLemma `per-function_wf_type` [⌜A⌝]⋅ THENA Auto)
   THEN Intro
   THEN (InstLemma `per-function-type-apply` [⌜A⌝;⌜B⌝]⋅ THENA Auto)
   THEN (InstLemma `per-function_wf` [⌜A⌝;⌜B⌝]⋅ THENA Auto)
   THEN (InstLemma `per-product_wf` [⌜A⌝;⌜B⌝]⋅ THENA Auto)
   THEN Intro
   THEN Thin 2
   THEN PromoteHyp (-1) 3) }

1
1. [A] : Type
2. [B] : per-function(A;a.Type)
3. [p] : per-product(A;a.B[a])
4. ∀[a:A]. (B[a] ∈ Type)
5. per-function(A;a.B[a]) ∈ Type
6. per-product(A;a.B[a]) ∈ Type
⊢ uand(p ~ <fst(p), snd(p)>;uand(fst(p) ∈ A;snd(p) ∈ B[fst(p)]))

---

Latex:

---

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


By

---

Latex:
(Intro
  THEN  (InstLemma  `per-function\_wf\_type`  [\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Intro
  THEN  (InstLemma  `per-function-type-apply`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `per-function\_wf`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `per-product\_wf`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Intro
  THEN  Thin  2
  THEN  PromoteHyp  (-1)  3)

---

Home Index