---

Step * of Lemma apply-alist-inl

No Annotations
∀[A,T:Type].  ∀eq:EqDecider(T). ∀x:T. ∀L:(T × A) List. ∀z:A.  ((apply-alist(eq;L;x) = (inl z) ∈ (A?)) ⇒ (<x, z> ∈ L))
BY
{ (InstLemma `isl-apply-alist` [] THEN RepeatFor 5 (ParallelLast') THEN D -1 THEN Auto THEN (D -3 THENA Auto)) }

1
1. [A] : Type
2. [T] : Type
3. eq : EqDecider(T)
4. x : T
5. L : (T × A) List
6. (↑isl(apply-alist(eq;L;x))) ⇒ (x ∈ map(λp.(fst(p));L))
7. (↑isl(apply-alist(eq;L;x))) ⇐ (x ∈ map(λp.(fst(p));L))
8. z : A
9. apply-alist(eq;L;x) = (inl z) ∈ (A?)
10. (<x, outl(apply-alist(eq;L;x))> ∈ L)
⊢ (<x, z> ∈ L)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,T:Type].
    \mforall{}eq:EqDecider(T).  \mforall{}x:T.  \mforall{}L:(T  \mtimes{}  A)  List.  \mforall{}z:A.    ((apply-alist(eq;L;x)  =  (inl  z))  {}\mRightarrow{}  (<x,  z>  \mmember{}  L))


By

---

Latex:
(InstLemma  `isl-apply-alist`  []
  THEN  RepeatFor  5  (ParallelLast')
  THEN  D  -1
  THEN  Auto
  THEN  (D  -3  THENA  Auto))

---

Home Index