---

Step * of Lemma bpa-equiv_inversion

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

---

Latex:

---

Latex:
\mforall{}p:\{2...\}.  \mforall{}a,b:basic-padic(p).    (bpa-equiv(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  RepeatFor  2  (D  -1)
  THEN  UnfoldTopAb  (-2)
  THEN  Trivial)

---

Home Index