Tactics for using strong induction to define index sequence

impermeable / coq-waterproof

GNU Lesser General Public License v3.0

29 stars 9 forks source link

Tactics for using strong induction to define index sequence #33

Closed jellooo038 closed 8 months ago

jellooo038 commented 8 months ago

Warning: uses fixed letters 'n' and 'k' for index sequence and induction variable. This is because we don't (yet) know how to control the choice of dummy variables inside an exists-quantifier.