---

Step * of Lemma hereditarily-mkterm

No Annotations
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ].
  ∀f:opr. ∀bts:bound-term(opr) List.
    (hereditarily(opr;s.P[s];mkterm(f;bts))
    ⇐⇒ P[mkterm(f;bts)] ∧ (∀bt:bound-term(opr). ((bt ∈ bts) ⇒ hereditarily(opr;s.P[s];snd(bt)))))
BY
{ 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)
⊢ hereditarily(opr;s.P[s];snd(bt))

2
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))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[P:term(opr)  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}f:opr.  \mforall{}bts:bound-term(opr)  List.
        (hereditarily(opr;s.P[s];mkterm(f;bts))
        \mLeftarrow{}{}\mRightarrow{}  P[mkterm(f;bts)]  \mwedge{}  (\mforall{}bt:bound-term(opr).  ((bt  \mmember{}  bts)  {}\mRightarrow{}  hereditarily(opr;s.P[s];snd(bt)))))


By

---

Latex:
Auto

---

Home Index