---

Step * 1 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 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 
BY
{ Try SqEqCD }

---

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  eq  (fst(u))  x
then  inl  (snd(u))
else  rec-case(v)  of
          []  =>  inr  \mcdot{} 
          p::ps  =>
            r.if  eq  (fst(p))  x  then  inl  (snd(p))  else  r  fi 
fi 


By

---

Latex:
Try  SqEqCD

---

Home Index