---

Step * of Lemma absolutelyfree_wf

∀[T:Type]. (absolutelyfree{i:l}(T) ∈ ℙ')
BY
{ (ProveWfLemma THEN Try ((SubsumeC ⌜ℕ ⟶ ℕ⌝⋅ THEN Auto THEN DoSubsume THEN Auto))) }

1
1. T : Type
2. T ⊆r (ℕ ⟶ ℕ)
3. P : T ⟶ ℙ
4. f : T
5. P f
⊢ EquivRel(∃k:ℕ. ∀g:T. ((f = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g));x,y.True)

2
1. T : Type
2. T ⊆r (ℕ ⟶ ℕ)
3. ∀P:T ⟶ ℙ. ∀f:T.  ((P f) ⇒ ⇃(∃k:ℕ. ∀g:T. ((f = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g))))
4. S : Type
5. S ⊆r (ℕ ⟶ ℕ)
6. P : S ⟶ ℙ
7. f : S
8. P f
⊢ EquivRel(∃k:ℕ. ∀g:S. ((f = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g));x,y.True)

---

Latex:

---

Latex:
\mforall{}[T:Type].  (absolutelyfree\{i:l\}(T)  \mmember{}  \mBbbP{}')


By

---

Latex:
(ProveWfLemma  THEN  Try  ((SubsumeC  \mkleeneopen{}\mBbbN{}  {}\mrightarrow{}  \mBbbN{}\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  DoSubsume  THEN  Auto)))

---

Home Index