open Structs;;

type tactic =
  | Intro of var_lambda
  | Assumption;;