---

Step * of Lemma ml-maprevappend-sq

∀[T,A:Type]. ∀[f:A ⟶ T].
  ∀[as:A List]. ∀[bs:T List].  (ml-maprevappend(f;as;bs) ~ map(f;rev(as)) @ bs) 
  supposing valueall-type(T) ∧ valueall-type(A) ∧ A
BY
{ (RepeatFor 4 (Intro)
   THEN UseWitness ⌜Ax⌝⋅
   THEN Unfold `uall` 0
   THEN RepeatFor 2 ((MemTypeCD THENW Auto))
   THEN MemCD
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN RepeatFor 2 (D -1)
   THEN (Assert valueall-type(A ⟶ T) BY
               (Auto THEN RenameVar `a' (-1) THEN D 0 THEN EAuto 1))) }

1
1. T : Type
2. A : Type
3. f : A ⟶ T
4. valueall-type(T)
5. valueall-type(A)
6. A
7. valueall-type(A ⟶ T)
⊢ ∀as:A List. ∀bs:T List.  (ml-maprevappend(f;as;bs) ~ map(f;rev(as)) @ bs)

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[f:A  {}\mrightarrow{}  T].
    \mforall{}[as:A  List].  \mforall{}[bs:T  List].    (ml-maprevappend(f;as;bs)  \msim{}  map(f;rev(as))  @  bs) 
    supposing  valueall-type(T)  \mwedge{}  valueall-type(A)  \mwedge{}  A


By

---

Latex:
(RepeatFor  4  (Intro)
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  Unfold  `uall`  0
  THEN  RepeatFor  2  ((MemTypeCD  THENW  Auto))
  THEN  MemCD
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  RepeatFor  2  (D  -1)
  THEN  (Assert  valueall-type(A  {}\mrightarrow{}  T)  BY
                          (Auto  THEN  RenameVar  `a'  (-1)  THEN  D  0  THEN  EAuto  1)))

---

Home Index