---

Step * of Lemma fpf-as-apply-alist

∀[A,B:Type]. ∀[f:a:A fp-> B]. ∀[eq:EqDecider(A)].
  (f = <fpf-domain(f), λx.outl(apply-alist(eq;map(λx.<x, f(x)>;fpf-domain(f));x))> ∈ a:A fp-> B)
BY
{ (Auto
   THEN DVar `f'
   THEN RepUR ``fpf-domain fpf-ap fpf`` 0
   THEN EqCD
   THEN Auto
   THEN (Assert map(λx.<x, f1 x>;d) ∈ (A × B) List BY
               (InstLemma `map_wf` [⌈{a:A| (a ∈ d)} ⌉;⌈A × B⌉;⌈λx.<x, f1 x>⌉;⌈d⌉]⋅ THEN Auto))⋅) }

1
1. A : Type
2. B : Type
3. d : A List
4. f1 : a:{a:A| (a ∈ d)}  ─→ B
5. eq : EqDecider(A)
6. map(λx.<x, f1 x>;d) ∈ (A × B) List
⊢ f1 = (λx.outl(apply-alist(eq;map(λx.<x, f1 x>;d);x))) ∈ (a:{a:A| (a ∈ d)}  ─→ B)

---

Latex:


\mforall{}[A,B:Type].  \mforall{}[f:a:A  fp->  B].  \mforall{}[eq:EqDecider(A)].
    (f  =  <fpf-domain(f),  \mlambda{}x.outl(apply-alist(eq;map(\mlambda{}x.<x,  f(x)>fpf-domain(f));x))>)


By

(Auto
  THEN  DVar  `f'
  THEN  RepUR  ``fpf-domain  fpf-ap  fpf``  0
  THEN  EqCD
  THEN  Auto
  THEN  (Assert  map(\mlambda{}x.<x,  f1  x>d)  \mmember{}  (A  \mtimes{}  B)  List  BY
                          (InstLemma  `map\_wf`  [\mkleeneopen{}\{a:A|  (a  \mmember{}  d)\}  \mkleeneclose{};\mkleeneopen{}A  \mtimes{}  B\mkleeneclose{};\mkleeneopen{}\mlambda{}x.<x,  f1  x>\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THEN  Auto))\mcdot{})

---

Home Index