---

Step * of Lemma eq_seq_wf

∀[T:Type]. ∀[eq:T ⟶ T ⟶ 𝔹].  (eq_seq(eq) ∈ (k:ℕ × (ℕk ⟶ T)) ⟶ (k:ℕ × (ℕk ⟶ T)) ⟶ 𝔹)
BY
{ xxx(xxxAutoxxx
      THEN xxx(Unfold `eq_seq` 0
               THEN RepeatFor 4 ((MemCD THENA Auto))
               THEN Try (AutoBoolCase ⌜(k1 =z k2)⌝⋅)
               THEN Auto)xxx
      )xxx }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].    (eq\_seq(eq)  \mmember{}  (k:\mBbbN{}  \mtimes{}  (\mBbbN{}k  {}\mrightarrow{}  T))  {}\mrightarrow{}  (k:\mBbbN{}  \mtimes{}  (\mBbbN{}k  {}\mrightarrow{}  T))  {}\mrightarrow{}  \mBbbB{})


By

---

Latex:
xxx(xxxAutoxxx
        THEN  xxx(Unfold  `eq\_seq`  0
                          THEN  RepeatFor  4  ((MemCD  THENA  Auto))
                          THEN  Try  (AutoBoolCase  \mkleeneopen{}(k1  =\msubz{}  k2)\mkleeneclose{}\mcdot{})
                          THEN  Auto)xxx
        )xxx

---

Home Index