Archived tweet #10595 from the @leastfixedpoint Twitter Archive

Tilting at dependently-typed theorem proving again. Stuck at the trivial matter of proving decidable equality for a data type of s-expressions over booleans. Coq forgets the necessary induction hypothesis when it comes to the lists-of-s-expressions case. :-(