Backward proofs for bakery to endpoint translation

[agomezl]

⟦c⟧ →* c' ⇒ ∃c''. c' →* ⟦c''⟧ ∧ c →* c''