bind_let rule

This rule already appears in elaborated proofs output by Carcara.

@bandreotti writes: bind_let: Akin to "congruence for lets"

This rule (or an alternative formulation that Carcara can use instead) should be added to the standard. @bandreotti has more information about the formal description of the rule.