change symbols.
add composition proof and change composable helper module.
add homomorphism proof.
add homomorphism for nothing case (even if it is kind of obvious)