fact: Fixpoint lookup (P : Prop) (l : list dyn) : M P := match l with | D :: l => mmatch D with | [? (p : P)] Dyn p =u> ret p | _ => lookup P l end | [] => raise NotFound end.
imports: Mtac2(Mtac2 Ttactics Sorts) Coq(List)