Step
*
1
1
1
of Lemma
free-from-atom-fpf-ap
1. a : Atom1@i
2. A : Type@i'
3. eq : EqDecider(A)@i
4. B : A ââ đ'@i 2
5. f : x:A fp-> B[x]@i'
6. a#f:x:A fp-> B[x]@i'
7. x : A@i'
8. a#x:A@i'
9. (x â fpf-domain(f))
10. y : {x:A| (x â fpf-domain(f))} @i
11. x = y â {x:A| (x â fpf-domain(f))} @i
⢠a#Îťz.f(z):v:{x:A| (x â fpf-domain(f))} ââ B[v]
BY
{ FreeFromAtomApElim âfââ
}
1
1. a : Atom1@i
2. A : Type@i'
3. eq : EqDecider(A)@i
4. B : A ââ đ'@i 2
5. f : x:A fp-> B[x]@i'
6. a#f:x:A fp-> B[x]@i'
7. x : A@i'
8. a#x:A@i'
9. (x â fpf-domain(f))
10. y : {x:A| (x â fpf-domain(f))} @i
11. x = y â {x:A| (x â fpf-domain(f))} @i
⢠a#Îťz,z@0. z(z@0):v1:x:A fp-> B[x] ââ v:{x:A| (x â fpf-domain(v1))} ââ B[v]
Latex:
1. a : Atom1@i
2. A : Type@i'
3. eq : EqDecider(A)@i
4. B : A {}\mrightarrow{} \mBbbU{}'@i 2
5. f : x:A fp-> B[x]@i'
6. a\#f:x:A fp-> B[x]@i'
7. x : A@i'
8. a\#x:A@i'
9. (x \mmember{} fpf-domain(f))
10. y : \{x:A| (x \mmember{} fpf-domain(f))\} @i
11. x = y@i
\mvdash{} a\#\mlambda{}z.f(z):v:\{x:A| (x \mmember{} fpf-domain(f))\} {}\mrightarrow{} B[v]
By
FreeFromAtomApElim \mkleeneopen{}f\mkleeneclose{}\mcdot{}
Home
Index