This is a simple test page for backward-compat of jsCoq 0.16 with earlier versions that did not use ES modules.

We are going to need a simpler auxiliary lemma, one that connects rev, :: (the list constructor, also known as cons), and snoc (the dual of cons, a function that appends an element at the end of a list). This is because the latter two participate in the definition of the former, rev.

This proposition is proven by way of the standard induction on the structure of the list l.

Now we prove the central equality with a similar induction.

Finally, we apply functional extensionality to produce the equality as it was written in the title.

There is only one syntactic difference, which is that, in Coq, we need to pass an explicit value to the implicit (generic) type parameter A of rev.