proposition: Lemma hd_rel_all a l : (forall x, In x l -> le a x) -> HdRel le a l.
proof: Proof. intros H. induction l; auto. constructor. apply H. auto with datatypes. Qed.
imports: Program Utf8 Equations.Prop.Equations Bvector List Relations Arith Wf_nat Lia Coq.Lists.SetoidList Coq.Sorting.Sorting Coq.Sorting.Permutation Coq.Sorting.PermutSetoid Bool EquivDec Permutation