\lstdefinelanguage{grafite} { mathescape=true, texcl=false, keywords={include, set}, morekeywords={record, with, match, let, rec, corec, inductive, definition, axiom, qed, intro, intros, symmetry, simplify, rewrite, apply, elim, assumption, left, cut, cases, auto, right, coercion, split, lemma, theorem, skip, by, done, we, conclude, assume, need, to, prove, unfold, return, and, notation, interpretation, lapply, repeat, try, as, clear, in}, %emph={[1]Type, Prop, nat, real}, emphstyle={[1]\textit}, literate= {->}{{$\to$}}3 {:>}{{$\mathrm{:>}$}}1 {>->}{{$\mapsto$}}2 {<=}{{$\leq$}}2 {>=}{{$\geq$}}2 {<>}{{$\neq$}}1 {\\/}{{$\vee$}}1 {<->}{{$\leftrightarrow$}}2 {FORALL\ }{{$\forall\,$}}1 {EXISTS\ }{{$\exists\,$}}1 {ALPHA}{{$\alpha$}}1 {LAMBDA}{{$\lambda\,$}}1 {LANGLE}{{$\langle$}}1 {RANGLE}{{$\rangle$}}1 {EQUIV}{{$\equiv$}}1 {SIGMA}{{$\Sigma$}}1 {PSI}{{$\Psi$}}1 {DOTS}{{$\ldots$}}1 {NOT}{{$\neg$}}1 {\\in}{{$\in$}}1 {/\\}{$\land$}1 {=>}{{$\,\Rightarrow\,$}}1 {≝}{{:=}}1 {δ}{{$\delta$}}1 {λ}{{$\lambda\,$}}1 {≰}{{$\nleq\,$}}1 {∨}{{$\lor\,$}}1 {≈}{{$\approx\,$}}1 {∀}{{$\forall\,$}}1 {∃}{{$\exists\,$}}1 {⇝}{{$\leadsto\,$}}1 {→}{{$\rightarrow\,$}}1 {∧}{{$\land\,$}}1 {≤}{{$\leq\,$}}1 {¬}{{$\lnot\,$}}1 {≪}{{$\ll\,$}}1 {≫}{{$\gg\,$}}1 {⇒}{{$\,\Rightarrow$}}1 {⊢}{{$\vdash$}}1 {...}{{$\ldots$}}1 {ℕ}{{$\mathbb{N}$}}1 {Σ}{{$\Sigma$}}1 {Ⓧ}{{$\bigotimes$}}1 , comment=[s]{(*}{*)}, showstringspaces=true, extendedchars=true, sensitive=false, captionpos=b, mathescape=true, %backgroundcolor=\color{gray}, frame=tblr, frameround=tttt, columns=flexible, basicstyle=\small, }