---

Step * 1 of Lemma Veldman-Coquand


1. X : Type
⊢ ∀q:wfd-tree(X)
    ∀[A,B:n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ]. ∀[R,S:0-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));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:(Auto THEN Try ((Unfold `wfd-tree` 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. ((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))

---

Latex:

---

Latex:

1.  X  :  Type
\mvdash{}  \mforall{}q:wfd-tree(X)
        \mforall{}[A,B:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  X)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R,S:0-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));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(0;Wsup(tt;\mcdot{});q)))


By

---

Latex:
TACTIC:(Auto  THEN  Try  ((Unfold  `wfd-tree`  0  THEN  Auto)))

---

Home Index