---

Step * of Lemma fpf-compatible-symmetry

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f,g:a:A fp-> B[a]].  g || f supposing f || g
BY
{ (Auto THEN (RepeatFor 3 ((ParallelOp (-1))))⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[f,g:a:A  fp->  B[a]].    g  ||  f  supposing  f  ||  g


By

---

Latex:
(Auto  THEN  (RepeatFor  3  ((ParallelOp  (-1))))\mcdot{}  THEN  Auto)

---

Home Index