---

Step * of Lemma mklist-eq

∀[n:ℕ]. ∀[f,g:ℕ ⟶ Base].  mklist(n;f) ~ mklist(n;g) supposing ∀[i:ℕn]. (f i ~ g i)
BY
{ (Intros
   THEN Try (Complete ((EqCD THEN Try (Complete (Auto)) THEN GenConclAtAddr [2;1] THEN GenConclAtAddr [2;2] THEN Auto)))
   THEN SqUnhide
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN Intros
   THEN Try (Complete ((EqCD
                        THEN Try (Complete (Auto))
                        THEN GenConclAtAddr [2;1]
                        THEN GenConclAtAddr [2;2]
                        THEN Auto)))) }

1
1. n : ℤ
2. 0 < n
3. ∀f,g:ℕ ⟶ Base.  ((∀[i:ℕn - 1]. (f i ~ g i)) ⇒ (mklist(n - 1;f) ~ mklist(n - 1;g)))
4. f : ℕ ⟶ Base@i
5. g : ℕ ⟶ Base@i
6. ∀[i:ℕn]. (f i ~ g i)@i
⊢ mklist(n;f) ~ mklist(n;g)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f,g:\mBbbN{}  {}\mrightarrow{}  Base].    mklist(n;f)  \msim{}  mklist(n;g)  supposing  \mforall{}[i:\mBbbN{}n].  (f  i  \msim{}  g  i)


By

---

Latex:
(Intros
  THEN  Try  (Complete  ((EqCD
                                            THEN  Try  (Complete  (Auto))
                                            THEN  GenConclAtAddr  [2;1]
                                            THEN  GenConclAtAddr  [2;2]
                                            THEN  Auto)))
  THEN  SqUnhide
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  Intros
  THEN  Try  (Complete  ((EqCD
                                            THEN  Try  (Complete  (Auto))
                                            THEN  GenConclAtAddr  [2;1]
                                            THEN  GenConclAtAddr  [2;2]
                                            THEN  Auto))))

---

Home Index