lib/html/library_index_footer.template

derive induction via backward proof, to ensure that the premises are in the right order for constructors like "X x y x" where x and y are mutually recursive

</body>
</html>