---

Step * of Lemma fpf-dom_functionality2

∀[A:Type]. ∀[eq1,eq2:EqDecider(A)]. ∀[f:a:A fp-> Top]. ∀[x:A].  {↑x ∈ dom(f) supposing ↑x ∈ dom(f)}
BY
{ xxx(((Unfold `guard` 0 THEN Auto THEN (InstLemma `fpf-dom_functionality` [⌜A⌝; ⌜λ2a.Top⌝; ⌜eq1⌝; ⌜eq2⌝; ⌜f⌝; ⌜x⌝])⋅)
       THENA Auto
       )
      THEN (HypSubst (-1) 0)
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[eq1,eq2:EqDecider(A)].  \mforall{}[f:a:A  fp->  Top].  \mforall{}[x:A].    \{\muparrow{}x  \mmember{}  dom(f)  supposing  \muparrow{}x  \mmember{}  dom(f)\}


By

---

Latex:
xxx(((Unfold  `guard`  0
            THEN  Auto
            THEN  (InstLemma  `fpf-dom\_functionality`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}\mlambda{}\msubtwo{}a.Top\mkleeneclose{};  \mkleeneopen{}eq1\mkleeneclose{};  \mkleeneopen{}eq2\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{};  \mkleeneopen{}x\mkleeneclose{}])\mcdot{})
          THENA  Auto
          )
        THEN  (HypSubst  (-1)  0)
        THEN  Auto)xxx

---

Home Index