proposition: Lemma traverse_traverse_var: forall `{Var V, Traverse V V, Traverse V T}, @TraverseFunctorial V _ T _ -> @TraverseRelative V T _ -> @TraverseIdentifiesVar V _ _ -> forall f g t l, traverse g l (traverse_var f l t) = traverse (fun l x => g l (f l x)) l t.
proof: Proof. intros. rewrite traverse_functorial. eapply (traverse_extensional _). eauto using traverse_identifies_var. Qed.
imports: Dblib.DblibTactics