| changeset 1502 | cc0dcf248da3 |
| parent 1501 | 7e7dc267ae6b |
| child 1503 | 8639077e0f43 |
| 1501:7e7dc267ae6b | 1502:cc0dcf248da3 |
|---|---|
15 |
15 |
16 - nested recursion, like types "trm list" in a constructor |
16 - nested recursion, like types "trm list" in a constructor |
17 |
17 |
18 - strong induction rules |
18 - strong induction rules |
19 |
19 |
20 - show support equations |
|
20 |
21 |
21 What are the proofs that are still proved by sorry? |
22 - automate the proofs that are currently proved with sorry: |
23 alpha_equivp, fv_rsp, alpha_bn_rsp, alpha_bn_reflp |