---

Step * of Lemma bigrel-induction

∀[T:Type]
  ∀P:(T ⟶ T ⟶ ℙ) ⟶ ℙ. ∀F:(T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ.
    ((∀Rs:ℕ ⟶ T ⟶ T ⟶ ℙ. ((∀n:ℕ. P[Rs[n]]) ⇒ P[isect-rel(ℕ;n.Rs[n])]))
    ⇒ (∀R:T ⟶ T ⟶ ℙ. (P[R] ⇒ P[F[R]]))
    ⇒ P[λx,y. True]
    ⇒ P[∨R.F[R]])
BY
{ (Auto
   THEN Unfold `bigrel` 0
   THEN BackThruSomeHyp
   THEN InductionOnNat
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}P:(T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  \mBbbP{}.  \mforall{}F:(T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.
        ((\mforall{}Rs:\mBbbN{}  {}\mrightarrow{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}n:\mBbbN{}.  P[Rs[n]])  {}\mRightarrow{}  P[isect-rel(\mBbbN{};n.Rs[n])]))
        {}\mRightarrow{}  (\mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  (P[R]  {}\mRightarrow{}  P[F[R]]))
        {}\mRightarrow{}  P[\mlambda{}x,y.  True]
        {}\mRightarrow{}  P[\mvee{}R.F[R]])


By

---

Latex:
(Auto
  THEN  Unfold  `bigrel`  0
  THEN  BackThruSomeHyp
  THEN  InductionOnNat
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index