\ \(\*\*[^\)] [^\(]\*\*\) \(\* \*\) theorem definition lemma fact remark variant axiom alias and as coercion prefer nocomposites coinductive corec default for include include' inductive inverter in interpretation let match names notation on qed rec record return source 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 nodefaults coercions comments debug cr elim hint instance locate match def forall lambda to exists Rightarrow Assign land lor lnot liff subst vdash iforall iexists " "