---

Step * of Lemma per-or-family_wf

∀[A,B:Type].  (per-or-family(A;B) ∈ per-function(per-value();a.Type))
BY
{ (Auto
   THEN (Assert per-function(per-value();a.Type) ∈ 𝕌' BY
               (BLemma `per-function_wf_type` THEN Auto))
   THEN (DupHyp (-1) THEN Unfold `per-function` -1)
   THEN (PointwiseFunctionalityForEquality' 2 THENW Auto)
   THEN (PointwiseFunctionalityForEquality' 1 THENW Auto)
   THEN ((Unfold `per-function` 0 THEN PerEqCD_member) THENW Auto)
   THEN Reduce 0
   THEN (D 0 THEN Reduce 0)
   THEN Auto) }

1
1. A : Base
2. A1 : Base
3. A = A1 ∈ Type
4. B : Base
5. B1 : Base
6. B = B1 ∈ Type
7. per-function(per-value();a.Type) ∈ 𝕌'
8. pertype(λf,g. function-eq(per-value();a.Type;f;g)) ∈ 𝕌'
9. a : Base
10. b : Base
11. a = b ∈ per-value()
⊢ (per-or-family(A;B) a) = (per-or-family(A1;B1) b) ∈ Type

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    (per-or-family(A;B)  \mmember{}  per-function(per-value();a.Type))


By

---

Latex:
(Auto
  THEN  (Assert  per-function(per-value();a.Type)  \mmember{}  \mBbbU{}'  BY
                          (BLemma  `per-function\_wf\_type`  THEN  Auto))
  THEN  (DupHyp  (-1)  THEN  Unfold  `per-function`  -1)
  THEN  (PointwiseFunctionalityForEquality'  2  THENW  Auto)
  THEN  (PointwiseFunctionalityForEquality'  1  THENW  Auto)
  THEN  ((Unfold  `per-function`  0  THEN  PerEqCD\_member)  THENW  Auto)
  THEN  Reduce  0
  THEN  (D  0  THEN  Reduce  0)
  THEN  Auto)

---

Home Index