Tools

Term algebra reasoning using Vampire

Invariant generation using Vampire

Catamorphism generation and fusion in Coq