folded.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

Lemma rev_rev {A} (l: list A) : List.rev (List.rev l) = l.A:Type
l:list A
rev (rev l) = l
Proof.A:Type
l:list A
rev (rev l) = l
  induction l; cbn.A:Type
nil = nil
A:Type
a:A
l:list A
IHl:rev (rev l) = l
rev (rev l ++ a :: nil) = a :: l
  - (* l ← [] *)A:Type
nil = nil
    reflexivity.
  - (* l ← _ :: _ *)A:Type
a:A
l:list A
IHl:rev (rev l) = l
rev (rev l ++ a :: nil) = a :: l
    rewrite rev_app_distr.A:Type
a:A
l:list A
IHl:rev (rev l) = l
rev (a :: nil) ++ rev (rev l) = a :: l
    rewrite IHl.A:Type
a:A
l:list A
IHl:rev (rev l) = l
rev (a :: nil) ++ l = a :: l
    cbn.A:Type
a:A
l:list A
IHl:rev (rev l) = l
a :: l = a :: l reflexivity.
Qed.