proposition: Lemma Hiv_hd i l : Hiv (i :: l) -> [/\ [/\ forall ht, ht_valid ht -> ht_valid (f2 eloss edraw ht i), forall ht, ht_valid ht -> f1 i = loss -> f2 eloss edraw ht i = eloss :> estate, forall ht, ht_valid ht -> f1 i = draw -> edraw <= f2 eloss edraw ht i <= drawwin & forall ht, ht_valid ht -> f1 i = win -> drawwin <= f2 eloss edraw ht i], [/\ forall ht, ht_valid ht -> ht_valid (f2 edraw ewin ht i), forall ht, ht_valid ht -> f1 i = win -> f2 edraw ewin ht i = ewin :> estate, forall ht, ht_valid ht -> f1 i = draw -> lossdraw <= f2 edraw ewin ht i <= draw & forall ht, ht_valid ht -> f1 i = loss -> f2 edraw ewin ht i <= lossdraw] & ((forall ht, ht_valid ht -> ht_valid (f2 eloss ewin ht i)) /\ forall ht, ht_valid ht -> f2 eloss ewin ht i = f1 i :> estate)].
proof: Proof. move=> [[H1 H2 H3 H4] [H5 H6 H7 H8] [H9 H10]]. by (repeat split) => *; (apply H1 || apply H2 || apply H3 || apply H4 || apply H5 || apply H6 || apply H7 || apply H8 || apply H9 || apply H10) => //; rewrite in_cons eqxx. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)