---

Step * 1 of Lemma absolutelyfree_wf


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)
BY
{ (GenConcl ⌜(∃k:ℕ. ∀g:T. ((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.  P  :  T  {}\mrightarrow{}  \mBbbP{}
4.  f  :  T
5.  P  f
\mvdash{}  EquivRel(\mexists{}k:\mBbbN{}.  \mforall{}g:T.  ((f  =  g)  {}\mRightarrow{}  (P  g));x,y.True)


By

---

Latex:
(GenConcl  \mkleeneopen{}(\mexists{}k:\mBbbN{}.  \mforall{}g:T.  ((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