---

Step * of Lemma list_ind_cons_lemma

No Annotations
∀A,x,b,a:Top.  (rec-case([a / b]) of [] => x | h::t => r.A[h;t;r] ~ A[a;b;rec-case(b) of [] => x | h::t => r.A[h;t;r]])
BY
{ (UnivCD THENA Auto) }

1
1. A : Top
2. x : Top
3. b : Top
4. a : Top
⊢ rec-case([a / b]) of
  [] => x
  h::t =>
   r.A[h;t;r] ~ A[a;b;rec-case(b) of
                      [] => x
                      h::t =>
                       r.A[h;t;r]]

---

Latex:

---

Latex:
No  Annotations
\mforall{}A,x,b,a:Top.
    (rec-case([a  /  b])  of
      []  =>  x
      h::t  =>
        r.A[h;t;r]  \msim{}  A[a;b;rec-case(b)  of
                                              []  =>  x
                                              h::t  =>
                                                r.A[h;t;r]])


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index