---

Step * 1 of Lemma list_accum_is_reduce


1. A : Type
2. f : A ⟶ A ⟶ A
3. Comm(A;λx,y. f[x;y])
4. Assoc(A;λx,y. f[x;y])
5. as : A List
6. n : A
7. a : A
8. x1 : A
9. x2 : A
⊢ f[f[a;x1];x2] = f[f[a;x2];x1] ∈ A
BY
{ (∀h:hyp. RepUR ``assoc comm`` h  THEN (RWO "4<" 0 THENA Auto) THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  A
3.  Comm(A;\mlambda{}x,y.  f[x;y])
4.  Assoc(A;\mlambda{}x,y.  f[x;y])
5.  as  :  A  List
6.  n  :  A
7.  a  :  A
8.  x1  :  A
9.  x2  :  A
\mvdash{}  f[f[a;x1];x2]  =  f[f[a;x2];x1]


By

---

Latex:
(\mforall{}h:hyp.  RepUR  ``assoc  comm``  h    THEN  (RWO  "4<"  0  THENA  Auto)  THEN  EqCD  THEN  Auto)

---

Home Index