work on rev involutive again. came up with a clever proof that works on paper, but which coq won't accept. tried 2 ways to make coq accept it, which didn't work. might need logic or rewriting