proposition: Lemma traverse_extensional: forall `{Traverse V T}, TraverseRelative -> forall f g, (forall l x, f l x = g l x) -> forall t l, traverse f l t = traverse g l t.
proof: Proof. intros. eapply traverse_relative with (p := 0). intros m ?. replace (m + 0) with m by lia. eauto. lia. Qed.
imports: Arith Lia Dblib.DblibTactics