---

Step * of Lemma bpa-equiv_weakening

∀p:{2...}. ∀a,b:basic-padic(p).  ((a = b ∈ basic-padic(p)) ⇒ bpa-equiv(p;b;a))
BY
{ ((D 0 THENA Auto) THEN (InstLemma `bpa-equiv-equiv` [⌜p⌝]⋅ THENA Auto) THEN D -1 THEN UnfoldTopAb (-2) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}p:\{2...\}.  \mforall{}a,b:basic-padic(p).    ((a  =  b)  {}\mRightarrow{}  bpa-equiv(p;b;a))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (InstLemma  `bpa-equiv-equiv`  [\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  UnfoldTopAb  (-2)
  THEN  Auto)

---

Home Index