Extending Bachmair's method for proof by consistency to the final algebra

Bachmair, 1988, Proof by consistency in equational theories, Proc. 3rd IEEE Symp. on Logic in Computer Science, 228 Fribourg, 1986, A strong restriction on the inductive completion procedure, 226, 105 Guttag, 1985, Larch in five easy pieces Hennicker, 1989, Observational implementations, 349, 59 Kapur, 1987, On sufficient-completeness and related properties of term rewriting systems, Acta Inform., 24, 395, 10.1007/BF00292110 Knuth, 1970, Simple word problems in universal algebras, 263 Küchlin, 1989, Inductive completion by ground proof transformation Lankford, 1975, Canonical inference Lysne, 1992, Proof by consistency in constructive systems with final algebra semantics, 632, 276 Musser, 1980, On proving inductive properties in abstract data types, Proc. 7th Ann. ACM Symp. on Principles of Programming Languages, 154 Puel, 1984, Proof in the final algebra, 227 Wirsing, 1990, Algebraic specification, Volume B