proposition: Lemma lookup_dep_prop (l : list {el : A & B el}) : (forall x, In x l -> P (projT2 x)) -> (forall a : A, P (@default a)) -> P (lookup_dep l).
proof: Proof. Proof with auto with datatypes. induction l; intros. apply H0. simpl. destruct a. destruct (@eqA_dec el x). unfold eq_rect, lookup_dep_obligation_1. set (w := eq_ind_r (fun el => x = el) eq_refl e). dependent inversion w. apply (H (existT b))... apply IHl... Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)