---

Step * of Lemma combine-list-flip

∀[A:Type]. ∀[f:A ⟶ A ⟶ A].
  (∀[as:A List]. ∀[a1,a2:A].
     (combine-list(x,y.f[x;y];[a1; [a2 / as]]) = combine-list(x,y.f[x;y];[a2; [a1 / as]]) ∈ A)) supposing 
     (Comm(A;λx,y. f[x;y]) and 
     Assoc(A;λx,y. f[x;y]))
BY
{ ((Auto THEN Unfold `combine-list` 0 THEN Reduce 0) THEN (EqCD THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    (\mforall{}[as:A  List].  \mforall{}[a1,a2:A].
          (combine-list(x,y.f[x;y];[a1;  [a2  /  as]])
          =  combine-list(x,y.f[x;y];[a2;  [a1  /  as]])))  supposing 
          (Comm(A;\mlambda{}x,y.  f[x;y])  and 
          Assoc(A;\mlambda{}x,y.  f[x;y]))


By

---

Latex:
((Auto  THEN  Unfold  `combine-list`  0  THEN  Reduce  0)  THEN  (EqCD  THEN  Auto)\mcdot{})

---

Home Index