]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
- bugfixed "aacr" allows to remove historical eta-conversions
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / cprs.ma
index a8eb52ab50dc467bb522c133e4e26d7a3265e42e..e4c5460d09769a3c0285211a191baf0845baf0da 100644 (file)
@@ -140,5 +140,5 @@ qed-.
    pr1_head_1 pr1_head_2 pr1_comp
    clear_pr3_trans pr3_cflat pr3_gen_bind
    pr3_head_1 pr3_head_2 pr3_head_21 pr3_head_12
-   pr3_iso_appl_bind pr3_iso_applv_appl_bind pr3_iso_applv_bind
+   pr3_iso_appl_bind pr3_iso_appls_appl_bind pr3_iso_appls_bind
 *)