return to top
source
When the goal mvarId type is an inductive datatype, constructor calls apply with the first matching constructor.
mvarId
constructor
apply