---

Step * 1 of Lemma fpf-as-apply-alist


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)
BY
{ xxx((Ext THEN Reduce 0)
      THEN Try (Complete (Auto))
      THEN Try (((EqCD THENA Auto) THEN Fold `member` 0))
      THEN (InstLemma `apply-alist-cases` [⌜A⌝;⌜eq⌝;⌜x⌝;⌜map(λx.<x, f1 x>;d)⌝]⋅ THENA Try (Complete (Auto)))
      THEN DVar `x'
      THEN D -1
      THEN Thin (-2))xxx }

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
7. x : A
8. (x ∈ d)
9. ∀[i:ℕ||map(λx.<x, f1 x>;d)||]
     (apply-alist(eq;map(λx.<x, f1 x>;d);x) ~ inl (snd(map(λx.<x, f1 x>;d)[i]))) supposing 
        (((fst(map(λx.<x, f1 x>;d)[i])) = x ∈ A) and 
        (∀j:ℕi. (¬((fst(map(λx.<x, f1 x>;d)[j])) = x ∈ A))))
⊢ (f1 x) = outl(apply-alist(eq;map(λx.<x, f1 x>;d);x)) ∈ B

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  d  :  A  List
4.  f1  :  a:\{a:A|  (a  \mmember{}  d)\}    {}\mrightarrow{}  B
5.  eq  :  EqDecider(A)
6.  map(\mlambda{}x.<x,  f1  x>d)  \mmember{}  (A  \mtimes{}  B)  List
\mvdash{}  f1  =  (\mlambda{}x.outl(apply-alist(eq;map(\mlambda{}x.<x,  f1  x>d);x)))


By

---

Latex:
xxx((Ext  THEN  Reduce  0)
        THEN  Try  (Complete  (Auto))
        THEN  Try  (((EqCD  THENA  Auto)  THEN  Fold  `member`  0))
        THEN  (InstLemma  `apply-alist-cases`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}map(\mlambda{}x.<x,  f1  x>d)\mkleeneclose{}]\mcdot{}
                    THENA  Try  (Complete  (Auto))
                    )
        THEN  DVar  `x'
        THEN  D  -1
        THEN  Thin  (-2))xxx

---

Home Index