---

Step * of Lemma mk_applies_fun2

∀[F,K,v:Top]. ∀[p,n:ℕ]. ∀[m:ℕn + 1].
  (mk_applies(F;λk.if (p + k =z p + n) then v else K (p + k) fi ;m) ~ mk_applies(F;λi.(K (p + i));m))
BY
{ ((UnivCD THENA Auto) THEN RepeatFor 2 ((D (-1) THENA Auto)) THEN (SubsumeHyp ⌜ℕ⌝ (-3)⋅ THENA Auto) THEN Thin (-2)) }

1
1. F : Top
2. K : Top
3. v : Top
4. p : ℕ
5. n : ℕ
6. m : ℕ
7. m < n + 1
⊢ mk_applies(F;λk.if (p + k =z p + n) then v else K (p + k) fi ;m) ~ mk_applies(F;λi.(K (p + i));m)

---

Latex:

---

Latex:
\mforall{}[F,K,v:Top].  \mforall{}[p,n:\mBbbN{}].  \mforall{}[m:\mBbbN{}n  +  1].
    (mk\_applies(F;\mlambda{}k.if  (p  +  k  =\msubz{}  p  +  n)  then  v  else  K  (p  +  k)  fi  ;m) 
    \msim{}  mk\_applies(F;\mlambda{}i.(K  (p  +  i));m))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepeatFor  2  ((D  (-1)  THENA  Auto))
  THEN  (SubsumeHyp  \mkleeneopen{}\mBbbN{}\mkleeneclose{}  (-3)\mcdot{}  THENA  Auto)
  THEN  Thin  (-2))

---

Home Index