| changeset 2120 | 2786ff1df475 |
| parent 2105 | e25b0fff0dd2 |
| child 2157 | a1d27083e688 |
| child 2165 | e838f7d90f81 |
| 2119:238062c4c9f2 | 2120:2786ff1df475 |
|---|---|
13 thm lam.supp |
13 thm lam.supp |
14 lemmas supp_fn' = lam.fv[simplified lam.supp] |
14 lemmas supp_fn' = lam.fv[simplified lam.supp] |
15 |
15 |
16 declare lam.perm[eqvt] |
16 declare lam.perm[eqvt] |
17 |
17 |
18 equivariance alpha_lam_raw |
|
19 |
18 |
20 section {* Strong Induction Principles*} |
19 section {* Strong Induction Principles*} |
21 |
20 |
22 (* |
21 (* |
23 Old way of establishing strong induction |
22 Old way of establishing strong induction |