---

Step * 1 of Lemma per-or-family_wf


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
BY
{ ((Assert a = b ∈ Base BY
          (SubsumeC ⌜per-value()⌝⋅ THEN Auto))
   THEN HypSubst' (-1) 0
   THEN (GenConcl ⌜b = x ∈ per-value()⌝⋅ THENA 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()
12. a = b ∈ Base
13. x : per-value()@i
14. b = x ∈ per-value()
⊢ (per-or-family(A;B) x) = (per-or-family(A1;B1) x) ∈ Type

---

Latex:

---

Latex:

1.  A  :  Base
2.  A1  :  Base
3.  A  =  A1
4.  B  :  Base
5.  B1  :  Base
6.  B  =  B1
7.  per-function(per-value();a.Type)  \mmember{}  \mBbbU{}'
8.  pertype(\mlambda{}f,g.  function-eq(per-value();a.Type;f;g))  \mmember{}  \mBbbU{}'
9.  a  :  Base
10.  b  :  Base
11.  a  =  b
\mvdash{}  (per-or-family(A;B)  a)  =  (per-or-family(A1;B1)  b)


By

---

Latex:
((Assert  a  =  b  BY
                (SubsumeC  \mkleeneopen{}per-value()\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  HypSubst'  (-1)  0
  THEN  (GenConcl  \mkleeneopen{}b  =  x\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index