---

Step * 1 of Lemma pi-simple-subst-aux_wf


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())))
BY
{ ((Auto THEN D 3)
   THEN OnMaybeHyp 5 (\h. (Unfold `pi-rank` h THEN Reduce h THEN Try (Fold `pi-rank` h)))
   THEN Try ((InstHyp [⌈n - 1⌉] 2⋅ THENA Complete (Auto)))
   THEN RecUnfold `pi-simple-subst-aux` 0
   THEN Reduce 0
   THEN Try (Unfold `let` 0)
   THEN Reduce 0
   THEN Auto
   THEN BackThruSomeHyp
   THEN Auto
   THEN RWO "pi-rank-pi-replace" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  \mforall{}n:\mBbbN{}n.  \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())))
\mvdash{}  \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())))


By

---

Latex:
((Auto  THEN  D  3)
  THEN  OnMaybeHyp  5  (\mbackslash{}h.  (Unfold  `pi-rank`  h  THEN  Reduce  h  THEN  Try  (Fold  `pi-rank`  h)))
  THEN  Try  ((InstHyp  [\mkleeneopen{}n  -  1\mkleeneclose{}]  2\mcdot{}  THENA  Complete  (Auto)))
  THEN  RecUnfold  `pi-simple-subst-aux`  0
  THEN  Reduce  0
  THEN  Try  (Unfold  `let`  0)
  THEN  Reduce  0
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Auto
  THEN  RWO  "pi-rank-pi-replace"  0
  THEN  Auto)

---

Home Index