equal
deleted
inserted
replaced
456 export_code ln_lam_aux nth_or_def ln_lam subst vara in SML |
456 export_code ln_lam_aux nth_or_def ln_lam subst vara in SML |
457 |
457 |
458 value "(atom N0 \<rightleftharpoons> atom N1) \<bullet> (App (Var N0) (Lam [N1]. (Var N1)))" |
458 value "(atom N0 \<rightleftharpoons> atom N1) \<bullet> (App (Var N0) (Lam [N1]. (Var N1)))" |
459 value "subst ((N0 \<leftrightarrow> N1) \<bullet> (App (Var N0) (Lam [N1]. (Var N1)))) N1 (Var N0)"*) |
459 value "subst ((N0 \<leftrightarrow> N1) \<bullet> (App (Var N0) (Lam [N1]. (Var N1)))) N1 (Var N0)"*) |
460 |
460 |
461 lemma [eqvt]: |
|
462 "p \<bullet> Let x y = Let (p \<bullet> x) (p \<bullet> y)" |
|
463 unfolding Let_def permute_fun_app_eq .. |
|
464 |
|
465 end |
461 end |
466 |
462 |
467 |
463 |
468 |
464 |