\ \(\*\*[^\)] [^\(]\*\*\) \(\* \*\) 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 destruct elim elimType exact exists fail fold fourier fwd generalize goal id intro intros inversion lapply linear left letin normalize reduce reflexivity replace rewrite ring right symmetry simplify split subst to transitivity unfold whd assume suppose by is or equivalent equivalently we prove proved need proceed induction inductive case base let such that by have and the thesis becomes hypothesis know case obtain conclude done try solve do repeat first focus unfocus progress inline procedural check hint set elim hint instance locate match def forall lambda to exists Rightarrow Assign land lor lnot liff subst vdash iforall iexists " "