All Questions
1
question
2
votes
1
answer
95
views
What does `induction ... in ...` do in Coq?
I'm self-studying the Semantics course, and met the following proof script in the warmup directory:
...