proposition: Lemma hput_correct ht t b e : ht_valid ht -> econtained (eval t b) e -> ht_valid (hput ht t b e).
proof: Proof. move=> Hv He b1 t1 e1. rewrite /hget /hput. case: eqP=> [->|_ /Hv] //=. by case: eqP=> [-> [<-]|_ /Hv]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)