\ \(\*\*[^\)] [^\(]\*\*\) \(\* \*\) theorem definition lemma fact remark variant axiom alias and as coercion nocomposites coinductive corec default for include include' inductive in interpretation let match names notation on qed rec record return to using with \[ \| \] \{ \} @ \$ Set Prop Type CProp absurd apply applyP assumption autobatch cases clear clearbody change compose constructor contradiction cut decompose destruct elim elimType exact exists fail fold fourier fwd generalize id intro intros inversion lapply linear left letin normalize reflexivity replace rewrite ring right symmetry simplify split 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 rule try solve do repeat first focus unfocus progress skip inline procedural check eval hint set auto elim hint instance locate match def forall lambda to exists Rightarrow Assign land lor lnot liff subst vdash iforall iexists " "