open Structs;;

type tactic =
  | Intro of var_lambda
  | Intros of var_lambda list
  | Assumption
  | Apply of var_lambda
  | Elim of var_lambda
  | Cut of ty
  | Split
  | Left
  | Right
  | Exact of lam;;