21:59 |
int-e |
Is there a good way of bringing the constructors of Enum.finite_3 (for example) into scope inside a proof? I have used let ?a1 = Enum.finite_3.a\<^sub>1 and ?a2 = Enum.finite_3.a\<^sub>2 and ?a3 = Enum.finite_3.a\<^sub>3 which makes them easy to type but I would like to actually bring the a\<^sub>1 into scope, if possible... |