---

Step * 1 1 of Lemma MTree-rank_wf


1. T : Type@i'
2. labels : {L:Atom List| 0 < ||L||} 
3. t2 : {a:Atom| (a ∈ labels)}  ─→ MultiTree(T)
4. ∀a:ℕ||labels||. (MTree-rank(t2 labels[a]) ∈ ℕ)
5. L : {a:Atom| (a ∈ labels)}  List@i
6. labels = L ∈ ({a:Atom| (a ∈ labels)}  List)@i
⊢ map(λa.MTree-rank(t2 a);L) ∈ ℕ List
BY
{ (RepeatFor 2 ((MemCD THEN Try (Complete (Auto))))
   THEN RepeatFor 3 (D -1)
   THEN (InstHyp [⌈i⌉] 4⋅ THENA Auto)
   THEN HypSubst' (-2) 0
   THEN Auto) }

---

Latex:



1.  T  :  Type@i'
2.  labels  :  \{L:Atom  List|  0  <  ||L||\} 
3.  t2  :  \{a:Atom|  (a  \mmember{}  labels)\}    {}\mrightarrow{}  MultiTree(T)
4.  \mforall{}a:\mBbbN{}||labels||.  (MTree-rank(t2  labels[a])  \mmember{}  \mBbbN{})
5.  L  :  \{a:Atom|  (a  \mmember{}  labels)\}    List@i
6.  labels  =  L@i
\mvdash{}  map(\mlambda{}a.MTree-rank(t2  a);L)  \mmember{}  \mBbbN{}  List


By

(RepeatFor  2  ((MemCD  THEN  Try  (Complete  (Auto))))
  THEN  RepeatFor  3  (D  -1)
  THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  4\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-2)  0
  THEN  Auto)

---

Home Index