---

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

∀[a:Atom1]. ∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ 𝕌']. ∀[f:x:A fp-> B[x]].
  ∀[x:A]. (a#f(x):B[x]) supposing ((↑x ∈ dom(f)) and a#x:A) supposing a#f:x:A fp-> B[x]
BY
{ (Intros THEN Unhide THEN Auto THEN (RWO "member-fpf-domain" (-1) THENA Auto)) }

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))
⊢ a#f(x):B[x]

---

Latex:

---

Latex:
\mforall{}[a:Atom1].  \mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  \mBbbU{}'].  \mforall{}[f:x:A  fp->  B[x]].
    \mforall{}[x:A].  (a\#f(x):B[x])  supposing  ((\muparrow{}x  \mmember{}  dom(f))  and  a\#x:A)  supposing  a\#f:x:A  fp->  B[x]


By

---

Latex:
(Intros  THEN  Unhide  THEN  Auto  THEN  (RWO  "member-fpf-domain"  (-1)  THENA  Auto))

---

Home Index