\ \(\* \*\) \(\*\* \*\*\) theorem definition lemma fact remark variant alias and as coercion coinductive corec default for include inductive in interpretation let match names notation on qed rec record to using with \[ \| \] \{ \} @ \$ Set Prop Type absurd apply assumption auto paramodulation 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 letin normalize reduce reflexivity replace rewrite ring symmetry simplify split to transitivity unfold 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 " "