search

impermeable / coq-waterproof

GNU Lesser General Public License v3.0
29 stars 9 forks source link

Specialize #51

Open jim-portegies opened 3 months ago

jim-portegies commented 3 months ago

A Waterproof version of specialization of forall statements. Usage is as in

It holds that (forall n : nat, n = n) (i).
Pick n := 3 in (i).
It holds that (3 = 3).