fact: Definition last {A} (t : gtactic A) : selector A := fun l => let n := dreduce (pred, mlength) (pred (mlength l)) in nth n (fun _=>t) l.
imports: Strings.String ssrmatching.ssrmatching Mtac2(Logic Datatypes List Utils Logic intf.Sorts) Strings.String NArith.BinNat NArith.BinNatDef