---

Step * of Lemma canonicalizable-function

∀[T:Type]
  ∀[B:T ⟶ Type]. retractible(T) ⇒ canonicalizable(x:T ⟶ B[x]) supposing ∀x:T. (B[x] ⊆r Base) 
  supposing (T ⊆r Base) ∧ value-type(T)
BY
{ TACTIC:(Auto THEN RepeatFor 2 (D -1) THEN With ⌜λg,x. eval z = f x in g z⌝ (D 0)⋅) }

1
.....wf..... 
1. T : Type
2. T ⊆r Base
3. value-type(T)
4. B : T ⟶ Type
5. ∀x:T. (B[x] ⊆r Base)
6. f : Base
7. ∀x:T. ((f x) = x ∈ T)
8. ∀x:Base. ((f x)↓ ⇒ (x ∈ T))
⊢ λg,x. eval z = f x in g z ∈ (x:T ⟶ B[x]) ⟶ Base

2
1. [T] : Type
2. T ⊆r Base
3. value-type(T)
4. [B] : T ⟶ Type
5. ∀x:T. (B[x] ⊆r Base)
6. f : Base
7. ∀x:T. ((f x) = x ∈ T)
8. ∀x:Base. ((f x)↓ ⇒ (x ∈ T))
⊢ ∀x:x:T ⟶ B[x]. (((λg,x. eval z = f x in g z) x) = x ∈ (x:T ⟶ B[x]))

3
.....wf..... 
1. T : Type
2. T ⊆r Base
3. value-type(T)
4. B : T ⟶ Type
5. ∀x:T. (B[x] ⊆r Base)
6. f : Base
7. ∀x:T. ((f x) = x ∈ T)
8. ∀x:Base. ((f x)↓ ⇒ (x ∈ T))
9. f1 : (x:T ⟶ B[x]) ⟶ Base
⊢ istype(∀x:x:T ⟶ B[x]. ((f1 x) = x ∈ (x:T ⟶ B[x])))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[B:T  {}\mrightarrow{}  Type].  retractible(T)  {}\mRightarrow{}  canonicalizable(x:T  {}\mrightarrow{}  B[x])  supposing  \mforall{}x:T.  (B[x]  \msubseteq{}r  Base) 
    supposing  (T  \msubseteq{}r  Base)  \mwedge{}  value-type(T)


By

---

Latex:
TACTIC:(Auto  THEN  RepeatFor  2  (D  -1)  THEN  With  \mkleeneopen{}\mlambda{}g,x.  eval  z  =  f  x  in  g  z\mkleeneclose{}  (D  0)\mcdot{})

---

Home Index