---

Step * 1 of Lemma simple-cbva-seq_wf


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)
BY
{ ((RW (AddrC [2] (LemmaC `funtype-unroll-last-eq`)) 0 THENA Auto) THEN AutoSplit) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  m  :  \{1...\}
3.  A  :  \mBbbN{}m  {}\mrightarrow{}  \{T:Type|  valueall-type(T)\} 
4.  L  :  i:\mBbbN{}m  {}\mrightarrow{}  funtype(i;A;A  i)
5.  F  :  (A  (m  -  1))  {}\mrightarrow{}  T
6.  mk\_lambdas(F;m  -  1)  \mmember{}  funtype(m  -  1;A;(A  (m  -  1))  {}\mrightarrow{}  T)
7.  mk\_lambdas(F;m  -  1)  =  mk\_lambdas(F;m  -  1)
\mvdash{}  funtype(m  -  1;A;(A  (m  -  1))  {}\mrightarrow{}  T)  \msubseteq{}r  funtype(m;A;T)


By

---

Latex:
((RW  (AddrC  [2]  (LemmaC  `funtype-unroll-last-eq`))  0  THENA  Auto)  THEN  AutoSplit)

---

Home Index