open Structs;; type tactic = | Intro of var_lambda | Assumption | Apply of var_lambda;;