---

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
{ (At ⌈𝕌{i''}⌉ (UniformUnivCD Auto)⋅ THEN Try (Complete (Auto)) THEN Repeat (MoveToConcl (-1))) }

1
∀a:Atom1. ∀A:Type. ∀eq:EqDecider(A). ∀B:A ─→ 𝕌'. ∀f:x:A fp-> B[x].
  (a#f:x:A fp-> B[x] ⇒ (∀x:A. (a#x:A ⇒ (↑x ∈ dom(f)) ⇒ a#f(x):B[x])))

---

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

(At  \mkleeneopen{}\mBbbU{}\{i''\}\mkleeneclose{}  (UniformUnivCD  Auto)\mcdot{}  THEN  Try  (Complete  (Auto))  THEN  Repeat  (MoveToConcl  (-1)))

---

Home Index