\ \(\* \*\) \(\*\* \*\*\) theorem definition lemma fact remark variant axiom alias and as coercion coinductive corec default for include 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 constructor contradiction cut decompose discriminate elim elimType exact exists fail fold fourier fwd generalize goal id injection intro intros inversion lapply left letin normalize reduce reflexivity replace rewrite ring right symmetry simplify split to transitivity unfold whd try solve do repeat first focus unfocus 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 " "