---

Step * of Lemma apply-alist-inr

No Annotations
∀[A,T:Type].
  ∀eq:EqDecider(T). ∀x:T. ∀u:Unit. ∀L:(T × A) List.
    ((apply-alist(eq;L;x) = (inr u ) ∈ (A?)) ⇒ (¬(∃z:A. (<x, z> ∈ L))))
BY
{ (InductionOnList THEN Reduce 0 THEN Auto) }

1
1. A : Type
2. T : Type
3. eq : EqDecider(T)
4. x : T
5. u : Unit
6. apply-alist(eq;[];x) = (inr u ) ∈ (A?)
⊢ ¬(∃z@0:A. (<x, z@0> ∈ []))

2
1. A : Type
2. T : Type
3. eq : EqDecider(T)
4. x : T
5. u : Unit
6. u1 : T × A
7. v : (T × A) List
8. (apply-alist(eq;v;x) = (inr u ) ∈ (A?)) ⇒ (¬(∃z:A. (<x, z> ∈ v)))
9. if eqof(eq) (fst(u1)) x then inl (snd(u1)) else apply-alist(eq;v;x) fi  = (inr u ) ∈ (A?)
⊢ ¬(∃z:A. (<x, z> ∈ [u1 / v]))

---

Latex:

---

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


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto)

---

Home Index