---

Step * of Lemma modify-combinator1_wf

∀[n:ℕ]
  ∀[A:ℕn ─→ Type]. ∀[m:ℕ]. ∀[B:ℕm ─→ Type]. ∀[T:Type]. ∀[f:(i:ℕn ─→ (A i + Top)) ─→ (i:ℕm ─→ (B i + Top)) ─→ T].
    (modify-combinator1(f) ∈ (i:ℕn - 1 ─→ if (i =z 0) then one_or_both(A 0;A 1) + Top else A (i + 1) + Top fi )
     ─→ (i:ℕm ─→ (B i + Top))
     ─→ T) 
  supposing 1 < n
BY
{ (Auto THEN Unfold `modify-combinator1` 0 THEN Auto) }

---

Latex:


\mforall{}[n:\mBbbN{}]
    \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[m:\mBbbN{}].  \mforall{}[B:\mBbbN{}m  {}\mrightarrow{}  Type].  \mforall{}[T:Type].  \mforall{}[f:(i:\mBbbN{}n  {}\mrightarrow{}  (A  i  +  Top))
                                                                                                                      {}\mrightarrow{}  (i:\mBbbN{}m  {}\mrightarrow{}  (B  i  +  Top))
                                                                                                                      {}\mrightarrow{}  T].
        (modify-combinator1(f)  \mmember{}  (i:\mBbbN{}n  -  1  {}\mrightarrow{}  if  (i  =\msubz{}  0)
                                                                                    then  one\_or\_both(A  0;A  1)  +  Top
                                                                                    else  A  (i  +  1)  +  Top
                                                                                    fi  )
          {}\mrightarrow{}  (i:\mBbbN{}m  {}\mrightarrow{}  (B  i  +  Top))
          {}\mrightarrow{}  T) 
    supposing  1  <  n


By

(Auto  THEN  Unfold  `modify-combinator1`  0  THEN  Auto)

---

Home Index