\ \(\* \*\) \(\*\* \*\*\) 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 return 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 left letin normalize reduce reflexivity replace rewrite ring right 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 lnot liff subst vdash iforall iexists " "