---

Step * 1 1 2 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) ∨ ([[S]] m s));q)
8. [[R]] 0 (λx.⊥)
9. n : ℕ
10. s : ℕn ⟶ X
11. (B n s) ∨ ([[S]] n s)
⊢ ((A n s) ∨ (B n s)) ∨ (([[R]] n s) ∧ ([[S]] n s))
BY
{ TACTIC:(ParallelLast THEN Auto THEN All (RepUR ``nary-rel-predicate``) THEN Auto) }

1
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

---

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{}  ([[S]]  m  s));q)
8.  [[R]]  0  (\mlambda{}x.\mbot{})
9.  n  :  \mBbbN{}
10.  s  :  \mBbbN{}n  {}\mrightarrow{}  X
11.  (B  n  s)  \mvee{}  ([[S]]  n  s)
\mvdash{}  ((A  n  s)  \mvee{}  (B  n  s))  \mvee{}  (([[R]]  n  s)  \mwedge{}  ([[S]]  n  s))


By

---

Latex:
TACTIC:(ParallelLast  THEN  Auto  THEN  All  (RepUR  ``nary-rel-predicate``)  THEN  Auto)

---

Home Index