---

Step * 1 1 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)
13. True
⊢ g x ∈ funtype(n - n - p - 1;λx.(A (x + (n - p - 1)));B)
BY
{ ((Assert ⌜(n - n - p) = p ∈ ℤ⌝⋅ THENA Auto)
   THEN (Assert ⌜(n - (n - p) + 1) = (p - 1) ∈ ℤ⌝⋅ THENA Auto)
   THEN HypSubst' (-1) 0
   THEN HypSubst' (-2) (-6)) }

1
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(p;λx.(A (x + (n - p)));B)
11. ¬(n = (n - p) ∈ ℤ)
12. x : A (n - p)
13. True
14. (n - n - p) = p ∈ ℤ
15. (n - (n - p) + 1) = (p - 1) ∈ ℤ
⊢ 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)
13.  True
\mvdash{}  g  x  \mmember{}  funtype(n  -  n  -  p  -  1;\mlambda{}x.(A  (x  +  (n  -  p  -  1)));B)


By

---

Latex:
((Assert  \mkleeneopen{}(n  -  n  -  p)  =  p\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}(n  -  (n  -  p)  +  1)  =  (p  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  HypSubst'  (-2)  (-6))

---

Home Index