\ \(\*\*[^\)] [^\(]\*\) \(\* \*\) theorem definition lemma fact remark variant axiom ntheorem nrecord ndefinition ninductive ncoinductive nlet nlemma naxiom 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 unification hint ncoercion ninverter nqed \[ \| \] \{ \} @ \$ Set Prop Type CProp Prop Type[0] CProp[0] Type[1] CProp[1] Type[2] CProp[2] 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 napply ncases nletin nauto nelim nwhd nnormalize nassumption ngeneralize nchange nrewrite ncut nlapply ndestruct try solve do repeat first focus unfocus progress skip inline procedural check eval hint set auto nodefaults coercions comments debug cr ncheck elim hint instance locate match def forall lambda to exists Rightarrow Assign land lor lnot liff subst vdash iforall iexists " "