---

Step * of Lemma apply_alist_cons_lemma

∀x,v,u,eq:Top.  (apply-alist(eq;[u / v];x) ~ if eqof(eq) (fst(u)) x then inl (snd(u)) else apply-alist(eq;v;x) fi )
BY
{ (UnivCD THENA Auto) }

1
1. x : Top@i
2. v : Top@i
3. u : Top@i
4. eq : Top@i
⊢ apply-alist(eq;[u / v];x) ~ if eqof(eq) (fst(u)) x then inl (snd(u)) else apply-alist(eq;v;x) fi 

---

Latex:

---

Latex:
\mforall{}x,v,u,eq:Top.
    (apply-alist(eq;[u  /  v];x)  \msim{}  if  eqof(eq)  (fst(u))  x
    then  inl  (snd(u))
    else  apply-alist(eq;v;x)
    fi  )


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index