Step * of Lemma retraction-fun-path

[T:Type]
  ∀f:T ⟶ T. ∀h:T ⟶ ℕ.
    ((∀x:T. (((f x) x ∈ T) ∨ (f x) < x))  (∀L:T List. ∀x,y:T.  (x y ∈ T) ∨ y < supposing y=f*(x) via L))
BY
(InductionOnList THEN Auto) }

1
1. [T] Type
2. T ⟶ T
3. T ⟶ ℕ
4. ∀x:T. (((f x) x ∈ T) ∨ (f x) < x)
5. T
6. T
7. y=f*(x) via []
⊢ (x y ∈ T) ∨ y < x

2
1. [T] Type
2. T ⟶ T
3. T ⟶ ℕ
4. ∀x:T. (((f x) x ∈ T) ∨ (f x) < x)
5. T
6. List
7. ∀x,y:T.  (x y ∈ T) ∨ y < supposing y=f*(x) via v
8. T
9. T
10. y=f*(x) via [u v]
⊢ (x y ∈ T) ∨ y < x


Latex:


Latex:
\mforall{}[T:Type]
    \mforall{}f:T  {}\mrightarrow{}  T.  \mforall{}h:T  {}\mrightarrow{}  \mBbbN{}.
        ((\mforall{}x:T.  (((f  x)  =  x)  \mvee{}  h  (f  x)  <  h  x))
        {}\mRightarrow{}  (\mforall{}L:T  List.  \mforall{}x,y:T.    (x  =  y)  \mvee{}  h  y  <  h  x  supposing  y=f*(x)  via  L))


By


Latex:
(InductionOnList  THEN  Auto)




Home Index