fact: Fixpoint last {A} (l : mlist A) : t A := match l with | [m:a] => ret a | _ :m: s => last s | _ => raise EmptyList end.
imports: Strings.String NArith.BinNat Mtac2(Logic Datatypes Logic List Utils MTele Pattern Specif)