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