---

Step * of Lemma pi-simple-subst-aux_wf

∀[P:pi_term()]. ∀[t,x:Name]. ∀[avoid:Name List].  (pi-simple-subst-aux(t;x;P;avoid) ∈ pi_term())
BY
{ (Assert ⌜∀n:ℕ. ∀P:pi_term().
             ((pi-rank(P) ≤ n) ⇒ (∀t,x:Name. ∀avoid:Name List.  (pi-simple-subst-aux(t;x;P;avoid) ∈ pi_term())))⌝⋅
   THEN Try ((Auto THEN (InstHyp [⌜pi-rank(P)⌝;⌜P⌝] 1⋅ THENA Auto) THEN BHyp -1  THEN Auto))
   THEN CompleteInductionOnNat) }

1
1. n : ℕ
2. ∀n:ℕn. ∀P:pi_term().
     ((pi-rank(P) ≤ n) ⇒ (∀t,x:Name. ∀avoid:Name List.  (pi-simple-subst-aux(t;x;P;avoid) ∈ pi_term())))
⊢ ∀P:pi_term(). ((pi-rank(P) ≤ n) ⇒ (∀t,x:Name. ∀avoid:Name List.  (pi-simple-subst-aux(t;x;P;avoid) ∈ pi_term())))

---

Latex:

---

Latex:
\mforall{}[P:pi\_term()].  \mforall{}[t,x:Name].  \mforall{}[avoid:Name  List].    (pi-simple-subst-aux(t;x;P;avoid)  \mmember{}  pi\_term())


By

---

Latex:
(Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}P:pi\_term().
                      ((pi-rank(P)  \mleq{}  n)
                      {}\mRightarrow{}  (\mforall{}t,x:Name.  \mforall{}avoid:Name  List.    (pi-simple-subst-aux(t;x;P;avoid)  \mmember{}  pi\_term())))\mkleeneclose{}\mcdot{}
  THEN  Try  ((Auto  THEN  (InstHyp  [\mkleeneopen{}pi-rank(P)\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]  1\mcdot{}  THENA  Auto)  THEN  BHyp  -1    THEN  Auto))
  THEN  CompleteInductionOnNat)

---

Home Index