Step
*
of Lemma
temp-lifting-gen-list-rev_wf
∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[g:funtype(n - m;λx.(A (x + m));B)].
(lifting-gen-list-rev(n;bags) m g ∈ bag(B))
BY
{ (InstLemma `lifting-gen-list-rev_wf` [] THEN Auto) }
Latex:
Latex:
\mforall{}[B:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[m:\mBbbN{}n + 1]. \mforall{}[A:\mBbbN{}n {}\mrightarrow{} Type]. \mforall{}[bags:k:\mBbbN{}n {}\mrightarrow{} bag(A k)].
\mforall{}[g:funtype(n - m;\mlambda{}x.(A (x + m));B)].
(lifting-gen-list-rev(n;bags) m g \mmember{} bag(B))
By
Latex:
(InstLemma `lifting-gen-list-rev\_wf` [] THEN Auto)
Home
Index