proposition: Lemma remove_nodefault : forall l (Hd:NoDefault l) (Hs:Sorted (Raw.ltk key_ord) l) x , NoDefault (Raw.remove key_comp x l).
proof: Proof. intros. unfold NoDefault. intros. unfold not. intro. apply Raw.remove_3 in H; auto. now apply Hd in H. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance