---

Step * 1 1 1 of Lemma per-function-ext


1. A : Type
2. per-function(A;a.Type) ∈ 𝕌'
3. B : per-function(A;x.Type)
4. ∀[a:A]. (B a ∈ Type)
5. per-function(A;a.B a) ∈ Type
6. ∀[f:per-function(A;a.B a)]. ∀[a:A].  (f a ∈ B a)
7. a : Base
8. b : Base
9. c : a = b ∈ (per-function(A;x.B x) × per-function(A;x.B x))
10. u1 : Base
11. u2 : Base
12. a = <u1, u2> ∈ (Base × Base)
⊢ λ%.Ax ∈ ∀v:∀[a@0:A]. ((u1 a@0) = (u2 a@0) ∈ (B a@0)). (u1 = u2 ∈ per-function(A;x.B x))
BY
{ TACTIC:(MoveToHyp 0 (-4)
          THEN HypSubst' (-2) (-1)
          THEN ThinVar `a'
          THEN (Assert ⌜(u1 ∈ per-function(A;a.B a)) ∧ (u2 ∈ per-function(A;a.B a))⌝⋅
                THENA (EqHD (-1) THEN AllReduce THEN Auto)
                )
          THEN D (-1)) }

1
1. A : Type
2. per-function(A;a.Type) ∈ 𝕌'
3. B : per-function(A;x.Type)
4. ∀[a:A]. (B a ∈ Type)
5. per-function(A;a.B a) ∈ Type
6. ∀[f:per-function(A;a.B a)]. ∀[a:A].  (f a ∈ B a)
7. b : Base
8. u1 : Base
9. u2 : Base
10. <u1, u2> = b ∈ (per-function(A;x.B x) × per-function(A;x.B x))
11. u1 ∈ per-function(A;a.B a)
12. u2 ∈ per-function(A;a.B a)
⊢ λ%.Ax ∈ ∀v:∀[a@0:A]. ((u1 a@0) = (u2 a@0) ∈ (B a@0)). (u1 = u2 ∈ per-function(A;x.B x))

---

Latex:

---

Latex:

1.  A  :  Type
2.  per-function(A;a.Type)  \mmember{}  \mBbbU{}'
3.  B  :  per-function(A;x.Type)
4.  \mforall{}[a:A].  (B  a  \mmember{}  Type)
5.  per-function(A;a.B  a)  \mmember{}  Type
6.  \mforall{}[f:per-function(A;a.B  a)].  \mforall{}[a:A].    (f  a  \mmember{}  B  a)
7.  a  :  Base
8.  b  :  Base
9.  c  :  a  =  b
10.  u1  :  Base
11.  u2  :  Base
12.  a  =  <u1,  u2>
\mvdash{}  \mlambda{}\%.Ax  \mmember{}  \mforall{}v:\mforall{}[a@0:A].  ((u1  a@0)  =  (u2  a@0)).  (u1  =  u2)


By

---

Latex:
TACTIC:(MoveToHyp  0  (-4)
                THEN  HypSubst'  (-2)  (-1)
                THEN  ThinVar  `a'
                THEN  (Assert  \mkleeneopen{}(u1  \mmember{}  per-function(A;a.B  a))  \mwedge{}  (u2  \mmember{}  per-function(A;a.B  a))\mkleeneclose{}\mcdot{}
                            THENA  (EqHD  (-1)  THEN  AllReduce  THEN  Auto)
                            )
                THEN  D  (-1))

---

Home Index