equal
deleted
inserted
replaced
12 thm lam.fv |
12 thm lam.fv |
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 |
|
18 declare permute_lam_raw.simps[eqvt] |
|
19 declare alpha_gen_eqvt[eqvt] |
|
20 equivariance alpha_lam_raw |
17 |
21 |
18 section {* Strong Induction Principles*} |
22 section {* Strong Induction Principles*} |
19 |
23 |
20 (* |
24 (* |
21 Old way of establishing strong induction |
25 Old way of establishing strong induction |