---

Step * of Lemma fun-path-member

∀[T:Type]. ∀f:T ⟶ T. ∀x,y:T. ∀L:T List.  {(x ∈ L) ∧ (y ∈ L)} supposing x=f*(y) via L
BY
{ xxx((UnivCD THENA Auto)
      THEN D -1
      THEN Auto
      THEN ((HypSubst (-3) 0 THEN Auto) THEN (DVar `L' THEN All Reduce) THEN Auto')⋅)xxx }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}f:T  {}\mrightarrow{}  T.  \mforall{}x,y:T.  \mforall{}L:T  List.    \{(x  \mmember{}  L)  \mwedge{}  (y  \mmember{}  L)\}  supposing  x=f*(y)  via  L


By

---

Latex:
xxx((UnivCD  THENA  Auto)
        THEN  D  -1
        THEN  Auto
        THEN  ((HypSubst  (-3)  0  THEN  Auto)  THEN  (DVar  `L'  THEN  All  Reduce)  THEN  Auto')\mcdot{})xxx

---

Home Index