proposition: Lemma nodefault_tail : forall x m d, NoDefault (x :: m) d -> NoDefault m d.
proof: Proof. unfold NoDefault. unfold not in *. intros. apply (H k). unfold Raw.MapsTo. apply InA_cons_tl. apply H0. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance