proposition: Lemma Hiv_cons i l : Hiv (i :: l) -> Hiv l.
proof: Proof. move=> [[H1 H2 H3 H4] [H5 H6 H7 H8] [H9 H10]]. by (repeat split) => i1 ht Hi1 *; (apply H1 || apply H2 || apply H3 || apply H4 || apply H5 || apply H6 || apply H7 || apply H8 || apply H9 || apply H10) => //; rewrite in_cons Hi1 orbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)