---

Step * 1 1 of Lemma free-from-atom-fpf-ap


1. a : Atom1
2. A : Type
3. eq : EqDecider(A)
4. B : A ⟶ 𝕌'
5. f : x:A fp-> B[x]
6. a#f:x:A fp-> B[x]
7. x : A
8. a#x:A
9. (x ∈ fpf-domain(f))
10. y : {x:A| (x ∈ fpf-domain(f))} 
11. x = y ∈ {x:A| (x ∈ fpf-domain(f))} 
⊢ a#λz.f(z):v:{x:A| (x ∈ fpf-domain(f))}  ⟶ B[v]
BY
{ FreeFromAtomApElim ⌜f⌝⋅ }

1
1. a : Atom1
2. A : Type
3. eq : EqDecider(A)
4. B : A ⟶ 𝕌'
5. f : x:A fp-> B[x]
6. a#f:x:A fp-> B[x]
7. x : A
8. a#x:A
9. (x ∈ fpf-domain(f))
10. y : {x:A| (x ∈ fpf-domain(f))} 
11. x = y ∈ {x:A| (x ∈ fpf-domain(f))} 
⊢ a#λz,z@0. z(z@0):v1:x:A fp-> B[x] ⟶ v:{x:A| (x ∈ fpf-domain(v1))}  ⟶ B[v]

---

Latex:

---

Latex:

1.  a  :  Atom1
2.  A  :  Type
3.  eq  :  EqDecider(A)
4.  B  :  A  {}\mrightarrow{}  \mBbbU{}'
5.  f  :  x:A  fp->  B[x]
6.  a\#f:x:A  fp->  B[x]
7.  x  :  A
8.  a\#x:A
9.  (x  \mmember{}  fpf-domain(f))
10.  y  :  \{x:A|  (x  \mmember{}  fpf-domain(f))\} 
11.  x  =  y
\mvdash{}  a\#\mlambda{}z.f(z):v:\{x:A|  (x  \mmember{}  fpf-domain(f))\}    {}\mrightarrow{}  B[v]


By

---

Latex:
FreeFromAtomApElim  \mkleeneopen{}f\mkleeneclose{}\mcdot{}

---

Home Index