---

Step * 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))
⊢ a#f(x):B[x]
BY
{ (GenConcl ⌜x = y ∈ {x:A| (x ∈ fpf-domain(f))} ⌝⋅ THENA Auto)
THEN FreeFromAtomApElim ⌜y⌝⋅ }

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.f(z):v:{x:A| (x ∈ fpf-domain(f))}  ⟶ 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))
\mvdash{}  a\#f(x):B[x]


By

---

Latex:
(GenConcl  \mkleeneopen{}x  =  y\mkleeneclose{}\mcdot{}  THENA  Auto)
THEN  FreeFromAtomApElim  \mkleeneopen{}y\mkleeneclose{}\mcdot{}

---

Home Index