open Structs;;

type tactic =
  | Intro of var_lambda
  | Assumption
  | Apply of var_lambda
  | Cut of ty;;