---

Step * 1 of Lemma lifting-gen-list-rev_wf


1. B : Type
2. n : ℕ
3. p : ℤ
4. 0 < p
5. 0 ≤ n - p - 1 < n + 1
⇒ (∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[g:funtype(n - n - p - 1;λx.(A (x + (n - p - 1)));B)].
      (lifting-gen-list-rev(n;bags) (n - p - 1) g ∈ bag(B)))
6. 0 ≤ (n - p)
7. n - p < n + 1
8. A : ℕn ⟶ Type
9. bags : k:ℕn ⟶ bag(A k)
10. g : funtype(n - n - p;λx.(A (x + (n - p)));B)
11. ¬(n = (n - p) ∈ ℤ)
12. x : A (n - p)
⊢ lifting-gen-list-rev(n;bags) ((n - p) + 1) (g x) ∈ bag(B)
BY
{ (Subst ⌜(n - p) + 1 ~ n - p - 1⌝ 0⋅ THEN Auto THEN Try ((BackThruSomeHyp THEN Auto))) }

1
.....wf..... 
1. B : Type
2. n : ℕ
3. p : ℤ
4. 0 < p
5. 0 ≤ n - p - 1 < n + 1
⇒ (∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[g:funtype(n - n - p - 1;λx.(A (x + (n - p - 1)));B)].
      (lifting-gen-list-rev(n;bags) (n - p - 1) g ∈ bag(B)))
6. 0 ≤ (n - p)
7. n - p < n + 1
8. A : ℕn ⟶ Type
9. bags : k:ℕn ⟶ bag(A k)
10. g : funtype(n - n - p;λx.(A (x + (n - p)));B)
11. ¬(n = (n - p) ∈ ℤ)
12. x : A (n - p)
⊢ g x ∈ funtype(n - n - p - 1;λx.(A (x + (n - p - 1)));B)

---

Latex:

---

Latex:

1.  B  :  Type
2.  n  :  \mBbbN{}
3.  p  :  \mBbbZ{}
4.  0  <  p
5.  0  \mleq{}  n  -  p  -  1  <  n  +  1
{}\mRightarrow{}  (\mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[bags:k:\mBbbN{}n  {}\mrightarrow{}  bag(A  k)].
        \mforall{}[g:funtype(n  -  n  -  p  -  1;\mlambda{}x.(A  (x  +  (n  -  p  -  1)));B)].
            (lifting-gen-list-rev(n;bags)  (n  -  p  -  1)  g  \mmember{}  bag(B)))
6.  0  \mleq{}  (n  -  p)
7.  n  -  p  <  n  +  1
8.  A  :  \mBbbN{}n  {}\mrightarrow{}  Type
9.  bags  :  k:\mBbbN{}n  {}\mrightarrow{}  bag(A  k)
10.  g  :  funtype(n  -  n  -  p;\mlambda{}x.(A  (x  +  (n  -  p)));B)
11.  \mneg{}(n  =  (n  -  p))
12.  x  :  A  (n  -  p)
\mvdash{}  lifting-gen-list-rev(n;bags)  ((n  -  p)  +  1)  (g  x)  \mmember{}  bag(B)


By

---

Latex:
(Subst  \mkleeneopen{}(n  -  p)  +  1  \msim{}  n  -  p  -  1\mkleeneclose{}  0\mcdot{}  THEN  Auto  THEN  Try  ((BackThruSomeHyp  THEN  Auto)))

---

Home Index