proposition: Lemma traverse_functorial_value_value: forall f g (t : my_value) l, traverse g l (traverse f l t) = traverse (fun l x => traverse g l (f l x)) l t with traverse_functorial_value_term: forall f g (t : my_term) l, traverse g l (traverse f l t) = traverse (fun l x => traverse g l (f l x)) l t.
proof: Proof. prove_traverse_functorial. prove_traverse_functorial. Qed.
imports: Dblib.DblibTactics Dblib.DeBruijn