---

Step * 1 1 of Lemma prank-psub


1. a : formula()
2. sub : formula()
3. a ⊆ sub
4. (a = sub ∈ formula()) ∨ prank(a) < prank(sub)
⊢ prank(a) < prank(sub) + 1
BY
{ (D (-1) THEN Auto THEN HypSubst' (-1) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  formula()
2.  sub  :  formula()
3.  a  \msubseteq{}  sub
4.  (a  =  sub)  \mvee{}  prank(a)  <  prank(sub)
\mvdash{}  prank(a)  <  prank(sub)  +  1


By

---

Latex:
(D  (-1)  THEN  Auto  THEN  HypSubst'  (-1)  0  THEN  Auto)

---

Home Index