---

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
{ (((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) }

---

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

(((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)

---

Home Index