fconstructor
is like constructor
(it calls apply
using the first matching constructor of an inductive datatype)
except that it does not reorder goals.
Instances For
econstructor
is like constructor
(it calls apply
using the first matching constructor of an inductive datatype)
except only non-dependent premises are added as new goals.