equal
deleted
inserted
replaced
375 "\<forall>f_lam. \<forall>f_app. \<exists>hom. ( |
375 "\<forall>f_lam. \<forall>f_app. \<exists>hom. ( |
376 (\<forall>x. hom (Var x) = f_var x) \<and> |
376 (\<forall>x. hom (Var x) = f_var x) \<and> |
377 (\<forall>l r. hom (App l r) = f_app l r (hom l) (hom r)) \<and> |
377 (\<forall>l r. hom (App l r) = f_app l r (hom l) (hom r)) \<and> |
378 (\<forall>x a. hom (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))) |
378 (\<forall>x a. hom (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))) |
379 )" |
379 )" |
380 apply (lifting hom) |
380 (*apply (lifting hom)*) |
|
381 sorry |
|
382 |
|
383 thm rlam.recs |
381 |
384 |
382 end |
385 end |