Software Foundation 学习笔记

Definition :

Inductive : 递归定义类型

simpl : 根据定义等自动化简

reflexivity : 等式自反性得证

rewrite : 使用引理重写