∀a:LOSet. ∀b:AbDGrp. ∀ps:|oal(a;b)|. (((--ps) ++ ps) = 00 ∈ |oal(a;b)|)
{ ((RepD THENM BLemma `lookups_same_a` THENM D 0) THENA Auto) }
1. a : LOSet
2. b : AbDGrp
3. ps : |oal(a;b)|
4. u : |a|
⊢ (((--ps) ++ ps)[u]) = (00[u]) ∈ |b|