try to understand length_snoc proof and do beq_nat_0_l. is there a way to do this without false = true (etc.)?