---

Step * 1 1 2 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.⊥)
⊢ tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));q)
BY
{ TACTIC:(Using [`A', ⌜λm,s. ((B m s) ∨ ([[S]] m s))⌝] (BLemma `tree-secures_functionality`)⋅ THEN Reduce 0 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) ∨ ([[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))

---

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{})
\mvdash{}  tree-secures(X;\mlambda{}m,s.  (((A  m  s)  \mvee{}  (B  m  s))  \mvee{}  (([[R]]  m  s)  \mwedge{}  ([[S]]  m  s)));q)


By

---

Latex:
TACTIC:(Using  [`A',  \mkleeneopen{}\mlambda{}m,s.  ((B  m  s)  \mvee{}  ([[S]]  m  s))\mkleeneclose{}]  (BLemma  `tree-secures\_functionality`)\mcdot{}
                THEN  Reduce  0
                THEN  Auto)

---

Home Index