proposition: Lemma traverse_relative_my_value_my_value: forall f g p (t : my_value) m l, (forall l x, f (l + p) x = g l x) -> m = l + p -> traverse f m t = traverse g l t with traverse_relative_my_value_my_term: forall f g p (t : my_term) m l, (forall l x, f (l + p) x = g l x) -> m = l + p -> traverse f m t = traverse g l t.
proof: Proof. prove_traverse_relative. prove_traverse_relative. Qed.
imports: Dblib.DblibTactics Dblib.DeBruijn