- For each each premise <command>H</command>
- of type <command>T</command> in the current context
- where <command>T</command> is a non-recursive inductive type
- withour right parameters, the tactic runs
+ For each each premise <command>H</command> of type
+ <command>T</command> in the current context where
+ <command>T</command> is a non-recursive inductive type without
+ right parameters and of sort Prop or CProp, the tactic runs