---

Step * 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. ((A m s) ∨ ([[R]] m s));Wsup(tt;⋅))
8. tree-secures(X;λm,s. ((B m s) ∨ ([[S]] m s));q)
⊢ tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(0;Wsup(tt;⋅);q))
BY
{ TACTIC:(RepUR ``Wsup`` -2
          THEN RecUnfold `tree-secures` (-2)
          THEN Reduce (-2)
          THEN (With ⌜λx.⊥⌝ (D (-2))⋅ THENA Auto)
          THEN RecUnfold `tree-tensor` 0
          THEN Reduce 0
          THEN D -1) }

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. A 0 (λx.⊥)
⊢ tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));q)

2
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)

---

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


By

---

Latex:
TACTIC:(RepUR  ``Wsup``  -2
                THEN  RecUnfold  `tree-secures`  (-2)
                THEN  Reduce  (-2)
                THEN  (With  \mkleeneopen{}\mlambda{}x.\mbot{}\mkleeneclose{}  (D  (-2))\mcdot{}  THENA  Auto)
                THEN  RecUnfold  `tree-tensor`  0
                THEN  Reduce  0
                THEN  D  -1)

---

Home Index