---

Step * of Lemma simple-cbva-seq_wf

∀[T:Type]. ∀[m:ℕ]. ∀[A:ℕm ⟶ ValueAllType]. ∀[L:i:ℕm ⟶ funtype(i;A;A i)]. ∀[F:if (m =z 0)
                                                                               then T
                                                                               else (A (m - 1)) ⟶ T
                                                                               fi ].
  (simple-cbva-seq(L;F;m) ∈ T)
BY
{ (Unfold `vatype` 0
   THEN (UnivCD THENA Auto)
   THEN Unfold `simple-cbva-seq` 0
   THEN (MoveToConcl (-1) THEN AutoSplit)
   THEN Auto
   THEN (InstLemma `mk_lambdas_wf` [⌜(A (m - 1)) ⟶ T⌝;⌜m - 1⌝;⌜A⌝;⌜F⌝]⋅ THENA Auto)
   THEN DoSubsume
   THEN Try (Hypothesis)) }

1
1. T : Type
2. m : {1...}
3. A : ℕm ⟶ {T:Type| valueall-type(T)} 
4. L : i:ℕm ⟶ funtype(i;A;A i)
5. F : (A (m - 1)) ⟶ T
6. mk_lambdas(F;m - 1) ∈ funtype(m - 1;A;(A (m - 1)) ⟶ T)
7. mk_lambdas(F;m - 1) = mk_lambdas(F;m - 1) ∈ funtype(m - 1;A;(A (m - 1)) ⟶ T)
⊢ funtype(m - 1;A;(A (m - 1)) ⟶ T) ⊆r funtype(m;A;T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[m:\mBbbN{}].  \mforall{}[A:\mBbbN{}m  {}\mrightarrow{}  ValueAllType].  \mforall{}[L:i:\mBbbN{}m  {}\mrightarrow{}  funtype(i;A;A  i)].  \mforall{}[F:if  (m  =\msubz{}  0)
                                                                                                                                                              then  T
                                                                                                                                                              else  (A  (m  -  1))  {}\mrightarrow{}  T
                                                                                                                                                              fi  ].
    (simple-cbva-seq(L;F;m)  \mmember{}  T)


By

---

Latex:
(Unfold  `vatype`  0
  THEN  (UnivCD  THENA  Auto)
  THEN  Unfold  `simple-cbva-seq`  0
  THEN  (MoveToConcl  (-1)  THEN  AutoSplit)
  THEN  Auto
  THEN  (InstLemma  `mk\_lambdas\_wf`  [\mkleeneopen{}(A  (m  -  1))  {}\mrightarrow{}  T\mkleeneclose{};\mkleeneopen{}m  -  1\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  DoSubsume
  THEN  Try  (Hypothesis))

---

Home Index