---

Step * 1 of Lemma hereditarily-mkterm


1. [opr] : Type
2. [P] : term(opr) ⟶ ℙ
3. f : opr
4. bts : bound-term(opr) List
5. hereditarily(opr;s.P[s];mkterm(f;bts))
6. bt : bound-term(opr)
7. (bt ∈ bts)
⊢ hereditarily(opr;s.P[s];snd(bt))
BY
{ (Enough to prove snd(bt) << mkterm(f;bts)
    Because (FLemma `hereditarily_functionality_wrt_subterm` [-4;-1] THEN Auto)) }

1
1. [opr] : Type
2. [P] : term(opr) ⟶ ℙ
3. f : opr
4. bts : bound-term(opr) List
5. hereditarily(opr;s.P[s];mkterm(f;bts))
6. bt : bound-term(opr)
7. (bt ∈ bts)
⊢ snd(bt) << mkterm(f;bts)

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  [P]  :  term(opr)  {}\mrightarrow{}  \mBbbP{}
3.  f  :  opr
4.  bts  :  bound-term(opr)  List
5.  hereditarily(opr;s.P[s];mkterm(f;bts))
6.  bt  :  bound-term(opr)
7.  (bt  \mmember{}  bts)
\mvdash{}  hereditarily(opr;s.P[s];snd(bt))


By

---

Latex:
(Enough  to  prove  snd(bt)  <<  mkterm(f;bts)
    Because  (FLemma  `hereditarily\_functionality\_wrt\_subterm`  [-4;-1]  THEN  Auto))

---

Home Index