---

Step * of Lemma mk_lambdas-sqequal-n2

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

---

Latex:

---

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


By

---

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

---

Home Index