\lstdefinelanguage{grafite} { mathescape=true, texcl=false, keywords={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, constructor, copy, from, letin, by, done, we, conclude, assume, need, to, prove, unfold, return, and, check, notation, interpretation, lapply, repeat, try, as, clear, in, change, whd, exists}, morekeywords={[2]include}, %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 {\\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 {𝟙}{{$\mathbf{1}$}}1 {𝟘}{{$\mathbf{0}$}}1 {/\\}{$\land$}1 {×}{{$\times\,$}}2 {\\x}{{$\times\,$}}2 {≝}{{:=}}1 {δ}{{$\delta$}}1 {λ}{{$\lambda\,$}}1 {≰}{{$\nleq\,$}}1 {∨}{{$\lor\,$}}1 {⋁}{{$\bigvee$}}1 {≈}{{$\approx\,$}}1 {∀}{{$\forall\,$}}1 {∃}{{$\exists\,$}}1 {⇝}{{$\leadsto\,$}}1 {→}{{$\rightarrow\,$}}1 {↔}{{$\leftrightarrow$}}1 {∧}{{$\land\,$}}1 {⋀}{{$\bigwedge$}}1 {≤}{{$\leq\,$}}1 {¬}{{$\lnot\,$}}1 {≪}{{$\ll\,$}}1 {≫}{{$\gg\,$}}1 {⇒}{{$\,\Rightarrow\,\,$}}2 {=>}{{$\,\Rightarrow\,\,$}}2 {⇒_0}{{$\,\Rightarrow_0\,\,$}}2 {=>_0}{{$\,\Rightarrow_0\,\,$}}2 {⇒_1}{{$\,\Rightarrow_1\,$}}1 {⇒_1.}{{$\,\Rightarrow_1\,$}}1 {⇒_\\r1}{{$\,\Rightarrow_1^{r}\,$}}1 {⇒_\\r2}{{$\,\Rightarrow_2^{r}\,$}}1 {=>_1}{{$\,\Rightarrow_1\,$}}1 {⇒_2}{{$\,\Rightarrow_2\,$}}1 {⇒_\\o2}{{$\,\Rightarrow_2^o\,$}}1 {⇒_\\c2}{{$\,\Rightarrow_2^c\,$}}1 {⇒_\\c3}{{$\,\Rightarrow_3^c\,$}}1 {⇒_\\obp2}{{$\,\Rightarrow_2^{obp}\,$}}1 {⇒_\\bp1}{{$\,\Rightarrow_1^{bp}\,$}}1 {⇒_\\bp2}{{$\,\Rightarrow_2^{bp}\,$}}1 {⇒_\\obt2}{{$\,\Rightarrow_2^{obt}\,$}}1 {⇒_2.}{{$\,\Rightarrow_2\,$}}1 {=>_2}{{$\,\Rightarrow_2\,$}}1 {=_1}{{$=$}}1 {=_2}{{$=$}}1 {⊢}{{$\vdash$}}1 {⊩}{{$\Vdash\,$}}2 {≬}{{$\between$}}2 {><}{{$>\!\!\!\!\!<\,$}}2 {⎻}{{$^-$}}1 {⎻*}{{$^{-*}$}}1 {\\sup\ ⎻}{{$\!^-\,$}}1 {\\sup\ ⎻*}{{$\!^{-*}\,$}}1 {\\sup\ *}{{$\!^{*}\,$}}1 {^*}{{$\!^{*}\,$}}1 {F*}{{F$^*$}}1 {G*}{{G$^*$}}1 {∘}{{$\circ\;$}}2 {Ω}{{$\Omega$}}1 {Ω^carrbt}{{$\Omega^{\mbox{carrbt}}$}}1 {Ω^A}{{$\Omega^A$}}1 {Ω^C}{{$\Omega^C$}}1 {Ω^U}{{$\Omega^U$}}1 {Ω^V}{{$\Omega^V$}}1 {Ω^X}{{$\Omega^X$}}1 {Ω^s}{{$\Omega^s$}}1 {‡}{{$\ddagger$}}1 {†}{{$\dagger$}}1 {⊆}{{$\subseteq\,$}}2 {♮}{{$\natural$}}1 {∩}{{$\cap$}}2 {∪}{{$\cup$}}2 {⋂}{{$\bigcap$}}2 {⋃}{{$\bigcup$}}2 {∈}{{$\in\,$}}2 {⎽o}{{$_o$}}1 {⎽f}{{$_f$}}1 {'\ \\sub\\c}{{'$\!_c$}}1 {\ \\sub\\c}{{$_c$}}1 {'\\sub\\c}{{'$\!_c$}}1 {\\sub\\c}{{$_c$}}1 {'\ \\sub\\f}{{'$\!_f$}}1 {\ \\sub\\f}{{$_f$}}1 {'\\sub\\f}{{'$\!_f$}}1 {\\sub\\f}{{$_f$}}1 {\\sup\ (form\ o)}{{$^{o_f}$}}1 {\\sup\ (concr\ o)}{{$^{o_c}$}}1 {(form\ o)}{{o$_f~$}}2 {(concr\ o)}{{o$_c~$}}2 {form\ o}{{o$_f~$}}2 {concr\ o}{{o$_c~$}}2 {Ω^(form\ o)}{{$\Omega^{o_f}~$}}2 {Ω^(concr\ o)}{{$\Omega^{o_c}~$}}2 {◊⎽t}{{$\Diamond_t$}}1 {□⎽t}{{$\boxempty_t$}}1 {⎽⇒}{{$_\Rightarrow$}}1 {o_operator_of_operator}{{o\_op\_of\_op}}2 {o_saturation_expansive}{{o\_sat\_expa}}2 {o_saturation_monotone}{{o\_sat\_monot}}2 {o_saturation_idempotent}{{o\_sat\_idemp}}2 {o_continuous_relation_of_continuous_relation}{{ocrel\_of\_crel}}2 {o_basic_topology_of_basic_topology}{{obtop\_of\_btop}}2 {basic_topology_of_basic_pair}{{btop\_of\_bp}}2 {o_basic_topology_of_o_basic_pair}{{o\_bt\_of\_o\_bp}}2 {^-1}{{$^{-1}$}}1 {^\ -1}{{$^{-1}$}}1 {\ \\sup\ -1}{{$^{-1}$}}1 {\\sup\ -1}{{$^{-1}$}}1 {\ \\sup-1}{{$^{-1}$}}1 {\\sup-1}{{$^{-1}$}}1 {...}{{$\ldots$}}1 , tabsize=1, comment=[s]{(*}{*)}, showstringspaces=true, emptylines=0, extendedchars=true, sensitive=false, captionpos=b, mathescape=true, keywordstyle=\bfseries, keywordstyle=[2]\bfseries, keywordstyle=[3]\bfseries, %backgroundcolor=\color{gray}, frame=tblr, %frameround=tttt, columns=flexible, basicstyle=\footnotesize\tt, }