---

Step * 1 of Lemma trivial-tree-secures


1. T : Type
2. [A] : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
3. A 0 (λx.⊥)
4. s : ℕ0 ⟶ T
⊢ A 0 s
BY
{ (NthHypEq (-2) THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  [A]  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbP{}
3.  A  0  (\mlambda{}x.\mbot{})
4.  s  :  \mBbbN{}0  {}\mrightarrow{}  T
\mvdash{}  A  0  s


By

---

Latex:
(NthHypEq  (-2)  THEN  EqCD  THEN  Auto)

---

Home Index