proposition: Lemma traverse_my_value_injective: forall f, (forall x1 x2 l, f l x1 = f l x2 -> x1 = x2) -> forall (t1 t2 : my_value) l, traverse_var f l t1 = traverse_var f l t2 -> t1 = t2 with traverse_my_term_injective: forall f, (forall x1 x2 l, f l x1 = f l x2 -> x1 = x2) -> forall (t1 t2 : my_term) l, traverse_var f l t1 = traverse_var f l t2 -> t1 = t2.
proof: Proof. prove_traverse_var_injective. prove_traverse_var_injective. Qed.
imports: Dblib.DblibTactics Dblib.DeBruijn