---

Step * 1 1 of Lemma apply_alist_cons_lemma


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 
BY
{ Try (RW (AddrC [2] (UnfoldsC ``apply-alist eqof``)) 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 eq (fst(u)) x
then inl (snd(u))
else rec-case(v) of
     [] => inr ⋅ 
     p::ps =>
      r.if eq (fst(p)) x then inl (snd(p)) else r fi 
fi 

---

Latex:

---

Latex:

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


By

---

Latex:
Try  (RW  (AddrC  [2]  (UnfoldsC  ``apply-alist  eqof``))  0)\mcdot{}

---

Home Index