---

Step * 1 1 2 1 1 of Lemma Veldman-Coquand


1. X : Type
2. q : wfd-tree(X)
3. [A] : n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ
4. [B] : n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ
5. [R] : 0-aryRel(X)
6. [S] : 0-aryRel(X)
7. tree-secures(X;λm,s. ((B m s) ∨ ((0 ≤ m) ∧ (S s)));q)
8. 0 ≤ 0
9. R (λx.⊥)
10. n : ℕ
11. s : ℕn ⟶ X
12. 0 ≤ n
13. S s
14. 0 ≤ n
⊢ R s
BY
{ TACTIC:(NthHypEq (-6) THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  q  :  wfd-tree(X)
3.  [A]  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  X)  {}\mrightarrow{}  \mBbbP{}
4.  [B]  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  X)  {}\mrightarrow{}  \mBbbP{}
5.  [R]  :  0-aryRel(X)
6.  [S]  :  0-aryRel(X)
7.  tree-secures(X;\mlambda{}m,s.  ((B  m  s)  \mvee{}  ((0  \mleq{}  m)  \mwedge{}  (S  s)));q)
8.  0  \mleq{}  0
9.  R  (\mlambda{}x.\mbot{})
10.  n  :  \mBbbN{}
11.  s  :  \mBbbN{}n  {}\mrightarrow{}  X
12.  0  \mleq{}  n
13.  S  s
14.  0  \mleq{}  n
\mvdash{}  R  s


By

---

Latex:
TACTIC:(NthHypEq  (-6)  THEN  EqCD  THEN  Auto)

---

Home Index