---

Step * of Lemma seq-normalize0

seq-normalize(0;λm.⊥) ~ λm.eval x = m in
                           ⊥
BY
{ (RepUR ``seq-normalize seq-append`` 0 THEN EqCD THEN SqReasoning) }

---

Latex:

---

Latex:
seq-normalize(0;\mlambda{}m.\mbot{})  \msim{}  \mlambda{}m.eval  x  =  m  in
                                                      \mbot{}


By

---

Latex:
(RepUR  ``seq-normalize  seq-append``  0  THEN  EqCD  THEN  SqReasoning)

---

Home Index