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