Transformation `apply` and inductive predicates
The apply
transformation does not seem to be able to apply constructors of inductive predicate.
inductive unit = tt : unit
goal g : unit
apply tt
gives Transformation raised a general error: apply