---

Step * 1 of Lemma apply_alist_cons_lemma


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 
BY
{ Try (RW (AddrC [1] (UnfoldC `apply-alist` ANDTHENC ReduceC)) 0)⋅ }

1
1. x : Top@i
2. v : Top@i
3. u : Top@i
4. eq : Top@i
⊢ if eq (fst(u)) x
then inl (snd(u))
else rec-case(v) of
     [] => inr ⋅ 
     h::t =>
      r.if eq (fst(h)) x then inl (snd(h)) else r fi 
fi  ~ if eqof(eq) (fst(u)) x then inl (snd(u)) else apply-alist(eq;v;x) fi 

---

Latex:

---

Latex:

1.  x  :  Top@i
2.  v  :  Top@i
3.  u  :  Top@i
4.  eq  :  Top@i
\mvdash{}  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:
Try  (RW  (AddrC  [1]  (UnfoldC  `apply-alist`  ANDTHENC  ReduceC))  0)\mcdot{}

---

Home Index