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