---

Step * 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;x.B x)
7. g : per-function(A;x.B x)
8. ∀[f:per-function(A;a.B a)]. ∀[a:A].  (f a ∈ B a)
9. ∀[a:A]. ((f a) = (g a) ∈ (B a))
⊢ f = g ∈ per-function(A;x.B x)
BY
{ (MoveToConcl (-1)
   THEN (Assert ⌜(λp.let f,g = p in ∀v:∀[a:A]. ((f a) = (g a) ∈ (B a)). (f = g ∈ per-function(A;x.B x))) <f, g>⌝⋅ THENM \000C(Reduce (-1) THEN Trivial))
   THEN GenConclAtAddr [2]
   THEN Thin (-1)
   THEN ThinVars [`f';`g']
   THEN PointwiseFunctionality (-1)
   THEN Reduce 0) }

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. [a] : Base
8. [b] : Base
9. [c] : a = b ∈ (per-function(A;x.B x) × per-function(A;x.B x))
⊢ let f,g = a 
  in ∀v:∀[a:A]. ((f a) = (g a) ∈ (B a)). (f = g ∈ per-function(A;x.B x))

2
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))
⊢ let f,g = a 
  in ∀v:∀[a:A]. ((f a) = (g a) ∈ (B a)). (f = g ∈ per-function(A;x.B x))
= let f,g = b 
  in ∀v:∀[a:A]. ((f a) = (g a) ∈ (B a)). (f = g ∈ per-function(A;x.B x))
∈ Type

---

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.  f  :  per-function(A;x.B  x)
7.  g  :  per-function(A;x.B  x)
8.  \mforall{}[f:per-function(A;a.B  a)].  \mforall{}[a:A].    (f  a  \mmember{}  B  a)
9.  \mforall{}[a:A].  ((f  a)  =  (g  a))
\mvdash{}  f  =  g


By

---

Latex:
(MoveToConcl  (-1)
  THEN  (Assert  \mkleeneopen{}(\mlambda{}p.let  f,g  =  p  in  \mforall{}v:\mforall{}[a:A].  ((f  a)  =  (g  a)).  (f  =  g))  <f,  g>\mkleeneclose{}\mcdot{}  THENM  (Reduce  (-1)  T\000CHEN  Trivial))
  THEN  GenConclAtAddr  [2]
  THEN  Thin  (-1)
  THEN  ThinVars  [`f';`g']
  THEN  PointwiseFunctionality  (-1)
  THEN  Reduce  0)

---

Home Index