---

Step * of Lemma fun-connected-step-back

No Annotations
∀[T:Type]. ∀f:T ⟶ T. ∀x,y:T.  (x is f*(y) ⇒ x is f*(f y) supposing ¬(x = y ∈ T))
BY
{ (Auto THEN D -2 THEN (Assert ¬↑null(L) BY (DVar `L' THEN RepUR ``fun-path`` -2 THEN Reduce 0 THEN Auto'))) }

1
1. [T] : Type
2. f : T ⟶ T
3. x : T
4. y : T
5. L : T List
6. x=f*(y) via L
7. ¬(x = y ∈ T)
8. ¬↑null(L)
⊢ x is f*(f y)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}f:T  {}\mrightarrow{}  T.  \mforall{}x,y:T.    (x  is  f*(y)  {}\mRightarrow{}  x  is  f*(f  y)  supposing  \mneg{}(x  =  y))


By

---

Latex:
(Auto
  THEN  D  -2
  THEN  (Assert  \mneg{}\muparrow{}null(L)  BY
                          (DVar  `L'  THEN  RepUR  ``fun-path``  -2  THEN  Reduce  0  THEN  Auto')))

---

Home Index