proposition: Lemma lookup_prop l : (forall x, In x l -> P (snd x)) -> P default -> P (lookup l).
proof: Proof. Proof with auto with datatypes. induction l; intros... simpl. destruct a. destruct (@eqA_dec el a). apply (H (a, b))... apply IHl... Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)