---

Step * of Lemma fpf-dom-list_wf

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f:a:A fp-> Top].  (fpf-dom-list(f) ∈ {a:A| ↑a ∈ dom(f)}  List)
BY
{ (((Auto
     THEN DVar `f'
     THEN Unfolds ``fpf-dom-list fpf-dom`` 0
     THEN Reduce 0
     THEN (InstLemma `list-set-type` [⌈A⌉; ⌈d⌉])⋅)
    THENA Auto
    )
   THEN DoSubsume
   THEN Auto
   THEN SubtypeReasoning
   THEN Auto
   THEN RWO "assert-deq-member" 0
   THEN Auto) }

---

Latex:


\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[f:a:A  fp->  Top].    (fpf-dom-list(f)  \mmember{}  \{a:A|  \muparrow{}a  \mmember{}  dom(f)\}    List)


By

(((Auto
      THEN  DVar  `f'
      THEN  Unfolds  ``fpf-dom-list  fpf-dom``  0
      THEN  Reduce  0
      THEN  (InstLemma  `list-set-type`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}d\mkleeneclose{}])\mcdot{})
    THENA  Auto
    )
  THEN  DoSubsume
  THEN  Auto
  THEN  SubtypeReasoning
  THEN  Auto
  THEN  RWO  "assert-deq-member"  0
  THEN  Auto)

---

Home Index