---

Step * of Lemma trivial-tree-secures

∀T:Type. ∀p:wfd-tree(T).  ∀[A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ]. ((A 0 (λx.⊥)) ⇒ tree-secures(T;A;p))
BY
{ (((D 0 THENA Auto) THEN (BLemma `wfd-tree-induction` THENA Auto))
   THEN Auto
   THEN RecUnfold `tree-secures` 0
   THEN RepUR ``Wsup`` 0
   THEN Auto
   THEN Try ((BackThruSomeHyp THEN Auto THEN RepUR ``predicate-or-shift`` 0 THEN Auto))) }

1
1. T : Type
2. [A] : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
3. A 0 (λx.⊥)
4. s : ℕ0 ⟶ T
⊢ A 0 s

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}p:wfd-tree(T).    \mforall{}[A:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbP{}].  ((A  0  (\mlambda{}x.\mbot{}))  {}\mRightarrow{}  tree-secures(T;A;p))


By

---

Latex:
(((D  0  THENA  Auto)  THEN  (BLemma  `wfd-tree-induction`  THENA  Auto))
  THEN  Auto
  THEN  RecUnfold  `tree-secures`  0
  THEN  RepUR  ``Wsup``  0
  THEN  Auto
  THEN  Try  ((BackThruSomeHyp  THEN  Auto  THEN  RepUR  ``predicate-or-shift``  0  THEN  Auto)))

---

Home Index