---

Step * 2 of Lemma hereditarily-mkterm


1. [opr] : Type
2. [P] : term(opr) ⟶ ℙ
3. f : opr
4. bts : bound-term(opr) List
5. P[mkterm(f;bts)]
6. ∀bt:bound-term(opr). ((bt ∈ bts) ⇒ hereditarily(opr;s.P[s];snd(bt)))
⊢ hereditarily(opr;s.P[s];mkterm(f;bts))
BY
{ ((D 0 THEN Auto)
   THEN (RWO "subterm-mkterm" (-1) THENA Auto)
   THEN ExRepD
   THEN (Assert hereditarily(opr;s.P[s];snd(bts[i])) BY
               Auto)
   THEN D -1
   THEN D -3
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((D  0  THEN  Auto)
  THEN  (RWO  "subterm-mkterm"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  (Assert  hereditarily(opr;s.P[s];snd(bts[i]))  BY
                          Auto)
  THEN  D  -1
  THEN  D  -3
  THEN  Auto)

---

Home Index