---

Step * 3 2 1 1 of Lemma Veldman-Coquand


1. X : Type
2. n : ℤ
3. [%1] : 0 < n
4. ∀p,q:wfd-tree(X).
     ∀[A,B:n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ]. ∀[R,S:n - 1-aryRel(X)].
       (tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s));p)
       ⇒ 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(n - 1;p;q)))
5. f : X ⟶ wfd-tree(X)
6. ∀b:X
     ∀[A,B:n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ]. ∀[R,S:n-aryRel(X)].
       (tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s));Wsup(tt;⋅))
       ⇒ tree-secures(X;λm,s. ((B m s) ∨ ([[S]] m s));f b)
       ⇒ tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(n;Wsup(tt;⋅);f b)))
7. [A] : n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ
8. [B] : n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ
9. [R] : n-aryRel(X)
10. [S] : n-aryRel(X)
11. ∀s:ℕ0 ⟶ X. ((A 0 s) ∨ ([[R]] 0 s))
12. ∀x:X. tree-secures(X;λm,s. ((B m s) ∨ ([[S]] m s))[x];f x)
13. s : ℕ0 ⟶ X
⊢ ((A 0 s) ∨ (B 0 s)) ∨ (([[R]] 0 s) ∧ ([[S]] 0 s))
BY
{ TACTIC:(∀h:hyp. (InstHyp [⌜s⌝] h⋅ THENA Declaration)  THEN SplitOrHyps⋅ THEN Auto) }

1
1. X : Type
2. n : ℤ
3. [%1] : 0 < n
4. ∀p,q:wfd-tree(X).
     ∀[A,B:n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ]. ∀[R,S:n - 1-aryRel(X)].
       (tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s));p)
       ⇒ 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(n - 1;p;q)))
5. f : X ⟶ wfd-tree(X)
6. ∀b:X
     ∀[A,B:n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ]. ∀[R,S:n-aryRel(X)].
       (tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s));Wsup(tt;⋅))
       ⇒ tree-secures(X;λm,s. ((B m s) ∨ ([[S]] m s));f b)
       ⇒ tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(n;Wsup(tt;⋅);f b)))
7. [A] : n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ
8. [B] : n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ
9. [R] : n-aryRel(X)
10. [S] : n-aryRel(X)
11. ∀s:ℕ0 ⟶ X. ((A 0 s) ∨ ([[R]] 0 s))
12. ∀x:X. tree-secures(X;λm,s. ((B m s) ∨ ([[S]] m s))[x];f x)
13. s : ℕ0 ⟶ X
14. [[R]] 0 s
⊢ ((A 0 s) ∨ (B 0 s)) ∨ (([[R]] 0 s) ∧ ([[S]] 0 s))

---

Latex:

---

Latex:

1.  X  :  Type
2.  n  :  \mBbbZ{}
3.  [\%1]  :  0  <  n
4.  \mforall{}p,q:wfd-tree(X).
          \mforall{}[A,B:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  X)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R,S:n  -  1-aryRel(X)].
              (tree-secures(X;\mlambda{}m,s.  ((A  m  s)  \mvee{}  ([[R]]  m  s));p)
              {}\mRightarrow{}  tree-secures(X;\mlambda{}m,s.  ((B  m  s)  \mvee{}  ([[S]]  m  s));q)
              {}\mRightarrow{}  tree-secures(X;\mlambda{}m,s.  (((A  m  s)  \mvee{}  (B  m  s))  \mvee{}  (([[R]]  m  s)  \mwedge{}  ([[S]]  m  s)));tree-tensor(n 
                    -  1;p;q)))
5.  f  :  X  {}\mrightarrow{}  wfd-tree(X)
6.  \mforall{}b:X
          \mforall{}[A,B:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  X)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R,S:n-aryRel(X)].
              (tree-secures(X;\mlambda{}m,s.  ((A  m  s)  \mvee{}  ([[R]]  m  s));Wsup(tt;\mcdot{}))
              {}\mRightarrow{}  tree-secures(X;\mlambda{}m,s.  ((B  m  s)  \mvee{}  ([[S]]  m  s));f  b)
              {}\mRightarrow{}  tree-secures(X;\mlambda{}m,s.  (((A  m  s)  \mvee{}  (B  m  s))
                                                            \mvee{}  (([[R]]  m  s)  \mwedge{}  ([[S]]  m  s)));tree-tensor(n;Wsup(tt;\mcdot{});f  b)))
7.  [A]  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  X)  {}\mrightarrow{}  \mBbbP{}
8.  [B]  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  X)  {}\mrightarrow{}  \mBbbP{}
9.  [R]  :  n-aryRel(X)
10.  [S]  :  n-aryRel(X)
11.  \mforall{}s:\mBbbN{}0  {}\mrightarrow{}  X.  ((A  0  s)  \mvee{}  ([[R]]  0  s))
12.  \mforall{}x:X.  tree-secures(X;\mlambda{}m,s.  ((B  m  s)  \mvee{}  ([[S]]  m  s))[x];f  x)
13.  s  :  \mBbbN{}0  {}\mrightarrow{}  X
\mvdash{}  ((A  0  s)  \mvee{}  (B  0  s))  \mvee{}  (([[R]]  0  s)  \mwedge{}  ([[S]]  0  s))


By

---

Latex:
TACTIC:(\mforall{}h:hyp.  (InstHyp  [\mkleeneopen{}s\mkleeneclose{}]  h\mcdot{}  THENA  Declaration)    THEN  SplitOrHyps\mcdot{}  THEN  Auto)

---

Home Index