---

Step * 2 of Lemma absolutelyfree_wf


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)
BY
{ (GenConcl ⌜(∃k:ℕ. ∀g:S. ((f = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g))) = X ∈ ℙ⌝⋅
   THEN Auto
   THEN SubsumeC ⌜ℕ ⟶ ℕ⌝⋅
   THEN Auto
   THEN DoSubsume
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  T  \msubseteq{}r  (\mBbbN{}  {}\mrightarrow{}  \mBbbN{})
3.  \mforall{}P:T  {}\mrightarrow{}  \mBbbP{}.  \mforall{}f:T.    ((P  f)  {}\mRightarrow{}  \00D9(\mexists{}k:\mBbbN{}.  \mforall{}g:T.  ((f  =  g)  {}\mRightarrow{}  (P  g))))
4.  S  :  Type
5.  S  \msubseteq{}r  (\mBbbN{}  {}\mrightarrow{}  \mBbbN{})
6.  P  :  S  {}\mrightarrow{}  \mBbbP{}
7.  f  :  S
8.  P  f
\mvdash{}  EquivRel(\mexists{}k:\mBbbN{}.  \mforall{}g:S.  ((f  =  g)  {}\mRightarrow{}  (P  g));x,y.True)


By

---

Latex:
(GenConcl  \mkleeneopen{}(\mexists{}k:\mBbbN{}.  \mforall{}g:S.  ((f  =  g)  {}\mRightarrow{}  (P  g)))  =  X\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  SubsumeC  \mkleeneopen{}\mBbbN{}  {}\mrightarrow{}  \mBbbN{}\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  DoSubsume
  THEN  Auto)

---

Home Index