\ \(\* \*\) \(\*\* \*\*\) theorem definition lemma fact remark alias coercion coinductive corec in inductive let match qed rec record with \[ \| \] \{ \} Set Prop Type absurd apply assumption auto change contradiction cut decompose discriminate elim elimType exact exists fold fourier goal injection intro intros left letin normalize reduce reflexivity replace rewrite right ring symmetry simplify split transitivity whd print check hint quit set elim hint instance locate match def forall lambda to exists Rightarrow Assign land lor subst " "