---

Step * of Lemma mk_lambdas-sqequal-n

∀[F1,F2:Base].  ∀n,m:ℕ.  ((F1 ~n F2) ⇒ (mk_lambdas(F1;m) ~n + m mk_lambdas(F2;m)))
BY
{ (RepeatFor 5 ((D 0 THENA Auto))
   THEN NatInd (-2)
   THEN Try ((Subst ⌜n + 0 ~ n⌝ 0⋅ THENA Auto))
   THEN RepUR ``mk_lambdas`` 0
   THEN Auto
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN AutoSplit
   THEN Fold `mk_lambdas` 0
   THEN SqequalNCanonicalCD
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[F1,F2:Base].    \mforall{}n,m:\mBbbN{}.    ((F1  \msim{}n  F2)  {}\mRightarrow{}  (mk\_lambdas(F1;m)  \msim{}n  +  m  mk\_lambdas(F2;m)))


By

---

Latex:
(RepeatFor  5  ((D  0  THENA  Auto))
  THEN  NatInd  (-2)
  THEN  Try  ((Subst  \mkleeneopen{}n  +  0  \msim{}  n\mkleeneclose{}  0\mcdot{}  THENA  Auto))
  THEN  RepUR  ``mk\_lambdas``  0
  THEN  Auto
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  Fold  `mk\_lambdas`  0
  THEN  SqequalNCanonicalCD
  THEN  Auto')

---

Home Index