in progress of adding join_op etc, stuck in middle of proof for join_opp is a function