---

Step * 1 2 of Lemma assert-palindrome-test


1. T : Type
2. eq : EqDecider(T)
3. L : T List
⊢ uiff(↑(list-deq(eq) rev(L) L);rev(L) = L ∈ (T List))
BY
{ xxx(RWO "deq_property<" 0 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
\mvdash{}  uiff(\muparrow{}(list-deq(eq)  rev(L)  L);rev(L)  =  L)


By

---

Latex:
xxx(RWO  "deq\_property<"  0  THEN  Auto)xxx

---

Home Index