---

Step * 2 of Lemma implies-bigrel


1. [T] : Type
2. F : (T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ
3. rel-monotone{i:l}(T;R.F[R])
4. R' : T ⟶ T ⟶ ℙ
5. R' => F[R']
6. ∀n:ℕ. R' => primrec(n;λx,y. True;λm,R. F[R])
⊢ R' => ⋂n:ℕ. primrec(n;λx,y. True;λm,R. F[R])
BY
{ (D 0 THEN RepUR ``isect-rel`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  F  :  (T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  rel-monotone\{i:l\}(T;R.F[R])
4.  R'  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
5.  R'  =>  F[R']
6.  \mforall{}n:\mBbbN{}.  R'  =>  primrec(n;\mlambda{}x,y.  True;\mlambda{}m,R.  F[R])
\mvdash{}  R'  =>  \mcap{}n:\mBbbN{}.  primrec(n;\mlambda{}x,y.  True;\mlambda{}m,R.  F[R])


By

---

Latex:
(D  0  THEN  RepUR  ``isect-rel``  0  THEN  Auto)

---

Home Index