proposition: Lemma HdRelElt (xk:key) (ye:elt) ys : HdRel lt (xk, ye) ys -> forall ye', HdRel lt (xk, ye') ys.
proof: Proof. induction ys as [ |[yk yee] ys IHys]; auto. simpl. intros H ye'. inversion H as [ |b l H1 H0]; subst. now constructor. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance