---

Step * of Lemma language1_wf

∀[fml:D:Type ─→ ℙ ─→ (D ─→ ℙ) ─→ (D ─→ ℙ) ─→ (D ─→ D ─→ ℙ) ─→ (D ─→ D ─→ ℙ) ─→ (D ─→ D ─→ ℙ) ─→ (D ─→ D ─→ D ─→ ℙ) ─→ ℙ]
  (language1{i:l}(D,A,B,C,P,Q,R,H.fml[D;A;B;C;P;Q;R;H]) ∈ ℙ')
BY
{ (ProveWfLemma THEN Try (Unfold `so_apply` 0) THEN Auto) }

---

Latex:


\mforall{}[fml:D:Type
            {}\mrightarrow{}  \mBbbP{}
            {}\mrightarrow{}  (D  {}\mrightarrow{}  \mBbbP{})
            {}\mrightarrow{}  (D  {}\mrightarrow{}  \mBbbP{})
            {}\mrightarrow{}  (D  {}\mrightarrow{}  D  {}\mrightarrow{}  \mBbbP{})
            {}\mrightarrow{}  (D  {}\mrightarrow{}  D  {}\mrightarrow{}  \mBbbP{})
            {}\mrightarrow{}  (D  {}\mrightarrow{}  D  {}\mrightarrow{}  \mBbbP{})
            {}\mrightarrow{}  (D  {}\mrightarrow{}  D  {}\mrightarrow{}  D  {}\mrightarrow{}  \mBbbP{})
            {}\mrightarrow{}  \mBbbP{}]
    (language1\{i:l\}(D,A,B,C,P,Q,R,H.fml[D;A;B;C;P;Q;R;H])  \mmember{}  \mBbbP{}')


By

(ProveWfLemma  THEN  Try  (Unfold  `so\_apply`  0)  THEN  Auto)

---

Home Index