frees_inv_bind frees_inv_flat frees_inv_bind_O
frees_lref_eq frees_lref_be frees_weak
frees_bind_sn frees_bind_dx frees_flat_sn frees_flat_dx
frees_inv_bind frees_inv_flat frees_inv_bind_O
frees_lref_eq frees_lref_be frees_weak
frees_bind_sn frees_bind_dx frees_flat_sn frees_flat_dx