---

Step * 1 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) ∨ ([[S]] m s));q)
8. A 0 (λx.⊥)
⊢ tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));q)
BY
{ TACTIC:(BLemma `trivial-tree-secures` THEN Reduce 0 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{}  ([[S]]  m  s));q)
8.  A  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:(BLemma  `trivial-tree-secures`  THEN  Reduce  0  THEN  Auto)

---

Home Index