fact: Definition Hiv (l : seq board) := [/\ [/\ forall i ht, i \in l -> ht_valid ht -> ht_valid (f2 eloss edraw ht i), forall i ht , i \in l -> ht_valid ht -> f1 i = loss -> f2 eloss edraw ht i = eloss :> estate, forall i ht , i \in l -> ht_valid ht -> f1 i = draw -> edraw <= f2 eloss edraw ht i <= drawwin & forall i ht, i \in l -> ht_valid ht -> f1 i = win -> drawwin <= f2 eloss edraw ht i], [/\ forall i ht, i \in l -> ht_valid ht -> ht_valid (f2 edraw ewin ht i), forall i ht, i \in l -> ht_valid ht -> f1 i = win -> f2 edraw ewin ht i = ewin :> estate, forall i ht, i \in l -> ht_valid ht -> f1 i = draw -> lossdraw <= f2 edraw ewin ht i <= draw & forall i ht, i \in l -> ht_valid ht -> f1 i = loss -> f2 edraw ewin ht i <= lossdraw] & ((forall i ht, i \in l -> ht_valid ht -> ht_valid (f2 eloss ewin ht i)) /\ forall i ht, i \in l -> ht_valid ht -> f2 eloss ewin ht i = f1 i :> estate)].
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)