Step
*
of Lemma
set-induction-1-ext
∀[P:Set{i:l} ⟶ ℙ']. ((∀T:Type. ∀f:T ⟶ Set{i:l}. ((∀t:T. P[f[t]])
⇒ P[f"(T)]))
⇒ (∀s:Set{i:l}. P[s]))
BY
{ Extract of Obid: set-induction-1
not unfolding W_ind
finishing with Auto
normalizes to:
λh,s. W_ind(λa,f,x. (h a f x);s) }
Latex:
Latex:
\mforall{}[P:Set\{i:l\} {}\mrightarrow{} \mBbbP{}']
((\mforall{}T:Type. \mforall{}f:T {}\mrightarrow{} Set\{i:l\}. ((\mforall{}t:T. P[f[t]]) {}\mRightarrow{} P[f"(T)])) {}\mRightarrow{} (\mforall{}s:Set\{i:l\}. P[s]))
By
Latex:
Extract of Obid: set-induction-1
not unfolding W\_ind
finishing with Auto
normalizes to:
\mlambda{}h,s. W\_ind(\mlambda{}a,f,x. (h a f x);s)
Home
Index