proposition: Lemma H5loss_win ht i l : Hiv (i :: l) -> ht_valid ht -> f2 eloss ewin ht i = f1 i :> estate.
proof: Proof. by move/Hiv_hd=> [] _ _ [_ H]; apply: H. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)