Move test_examplefiles to new tests/lexers scheme.examplefiles

1 files changed, 5001 insertions, 0 deletions

diff --git a/tests/lexers/coq/example.txt b/tests/lexers/coq/example.txt
new file mode 100644
index 00000000..45918832
--- /dev/null
+++ b/tests/lexers/coq/example.txt
@@ -0,0 +1,5001 @@
+---input---
+(* -*- coding: utf-8 -*- *)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** *  Typeclass-based relations, tactics and standard instances
+
+   This is the basic theory needed to formalize morphisms and setoids.
+
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
+
+(* $Id: RelationClasses.v 14641 2011-11-06 11:59:10Z herbelin $ *)
+
+Require Export Coq.Classes.Init.
+Require Import Coq.Program.Basics.
+Require Import Coq.Program.Tactics.
+Require Import Coq.Relations.Relation_Definitions.
+
+(** We allow to unfold the [relation] definition while doing morphism search. *)
+
+Notation inverse R := (flip (R:relation _) : relation _).
+
+Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False.
+
+(** Opaque for proof-search. *)
+Typeclasses Opaque complement.
+
+(** These are convertible. *)
+
+Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R).
+Proof. reflexivity. Qed.
+
+(** We rebind relations in separate classes to be able to overload each proof. *)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Class Reflexive {A} (R : relation A) :=
+  reflexivity : forall x, R x x.
+
+Class Irreflexive {A} (R : relation A) :=
+  irreflexivity : Reflexive (complement R).
+
+Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances.
+
+Class Symmetric {A} (R : relation A) :=
+  symmetry : forall x y, R x y -> R y x.
+
+Class Asymmetric {A} (R : relation A) :=
+  asymmetry : forall x y, R x y -> R y x -> False.
+
+Class Transitive {A} (R : relation A) :=
+  transitivity : forall x y z, R x y -> R y z -> R x z.
+
+Hint Resolve @irreflexivity : ord.
+
+Unset Implicit Arguments.
+
+(** A HintDb for relations. *)
+
+Ltac solve_relation :=
+  match goal with
+  | [ |- ?R ?x ?x ] => reflexivity
+  | [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H
+  end.
+
+Hint Extern 4 => solve_relation : relations.
+
+(** We can already dualize all these properties. *)
+
+Generalizable Variables A B C D R S T U l eqA eqB eqC eqD.
+
+Lemma flip_Reflexive `{Reflexive A R} : Reflexive (flip R).
+Proof. tauto. Qed.
+
+Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances.
+
+Program Definition flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) :=
+  irreflexivity (R:=R).
+
+Program Definition flip_Symmetric `(Symmetric A R) : Symmetric (flip R) :=
+  fun x y H => symmetry (R:=R) H.
+
+Program Definition flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R) :=
+  fun x y H H' => asymmetry (R:=R) H H'.
+
+Program Definition flip_Transitive `(Transitive A R) : Transitive (flip R) :=
+  fun x y z H H' => transitivity (R:=R) H' H.
+
+Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances.
+Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances.
+Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances.
+Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances.
+
+Definition Reflexive_complement_Irreflexive `(Reflexive A (R : relation A))
+   : Irreflexive (complement R).
+Proof. firstorder. Qed.
+
+Definition complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R).
+Proof. firstorder. Qed.
+
+Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances.
+Hint Extern 3 (Irreflexive (complement _)) => class_apply Reflexive_complement_Irreflexive : typeclass_instances.
+
+(** * Standard instances. *)
+
+Ltac reduce_hyp H :=
+  match type of H with
+    | context [ _ <-> _ ] => fail 1
+    | _ => red in H ; try reduce_hyp H
+  end.
+
+Ltac reduce_goal :=
+  match goal with
+    | [ |- _ <-> _ ] => fail 1
+    | _ => red ; intros ; try reduce_goal
+  end.
+
+Tactic Notation "reduce" "in" hyp(Hid) := reduce_hyp Hid.
+
+Ltac reduce := reduce_goal.
+
+Tactic Notation "apply" "*" constr(t) :=
+  first [ refine t | refine (t _) | refine (t _ _) | refine (t _ _ _) | refine (t _ _ _ _) |
+    refine (t _ _ _ _ _) | refine (t _ _ _ _ _ _) | refine (t _ _ _ _ _ _ _) ].
+
+Ltac simpl_relation :=
+  unfold flip, impl, arrow ; try reduce ; program_simpl ;
+    try ( solve [ intuition ]).
+
+Local Obligation Tactic := simpl_relation.
+
+(** Logical implication. *)
+
+Program Instance impl_Reflexive : Reflexive impl.
+Program Instance impl_Transitive : Transitive impl.
+
+(** Logical equivalence. *)
+
+Program Instance iff_Reflexive : Reflexive iff.
+Program Instance iff_Symmetric : Symmetric iff.
+Program Instance iff_Transitive : Transitive iff.
+
+(** Leibniz equality. *)
+
+Instance eq_Reflexive {A} : Reflexive (@eq A) := @eq_refl A.
+Instance eq_Symmetric {A} : Symmetric (@eq A) := @eq_sym A.
+Instance eq_Transitive {A} : Transitive (@eq A) := @eq_trans A.
+
+(** Various combinations of reflexivity, symmetry and transitivity. *)
+
+(** A [PreOrder] is both Reflexive and Transitive. *)
+
+Class PreOrder {A} (R : relation A) : Prop := {
+  PreOrder_Reflexive :> Reflexive R ;
+  PreOrder_Transitive :> Transitive R }.
+
+(** A partial equivalence relation is Symmetric and Transitive. *)
+
+Class PER {A} (R : relation A) : Prop := {
+  PER_Symmetric :> Symmetric R ;
+  PER_Transitive :> Transitive R }.
+
+(** Equivalence relations. *)
+
+Class Equivalence {A} (R : relation A) : Prop := {
+  Equivalence_Reflexive :> Reflexive R ;
+  Equivalence_Symmetric :> Symmetric R ;
+  Equivalence_Transitive :> Transitive R }.
+
+(** An Equivalence is a PER plus reflexivity. *)
+
+Instance Equivalence_PER `(Equivalence A R) : PER R | 10 :=
+  { PER_Symmetric := Equivalence_Symmetric ;
+    PER_Transitive := Equivalence_Transitive }.
+
+(** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
+
+Class Antisymmetric A eqA `{equ : Equivalence A eqA} (R : relation A) :=
+  antisymmetry : forall {x y}, R x y -> R y x -> eqA x y.
+
+Program Definition flip_antiSymmetric `(Antisymmetric A eqA R) :
+  Antisymmetric A eqA (flip R).
+Proof. firstorder. Qed.
+
+(** Leibinz equality [eq] is an equivalence relation.
+   The instance has low priority as it is always applicable
+   if only the type is constrained. *)
+
+Program Instance eq_equivalence : Equivalence (@eq A) | 10.
+
+(** Logical equivalence [iff] is an equivalence relation. *)
+
+Program Instance iff_equivalence : Equivalence iff.
+
+(** We now develop a generalization of results on relations for arbitrary predicates.
+   The resulting theory can be applied to homogeneous binary relations but also to
+   arbitrary n-ary predicates. *)
+
+Local Open Scope list_scope.
+
+(* Notation " [ ] " := nil : list_scope. *)
+(* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *)
+
+(** A compact representation of non-dependent arities, with the codomain singled-out. *)
+
+Fixpoint arrows (l : list Type) (r : Type) : Type :=
+  match l with
+    | nil => r
+    | A :: l' => A -> arrows l' r
+  end.
+
+(** We can define abbreviations for operation and relation types based on [arrows]. *)
+
+Definition unary_operation A := arrows (A::nil) A.
+Definition binary_operation A := arrows (A::A::nil) A.
+Definition ternary_operation A := arrows (A::A::A::nil) A.
+
+(** We define n-ary [predicate]s as functions into [Prop]. *)
+
+Notation predicate l := (arrows l Prop).
+
+(** Unary predicates, or sets. *)
+
+Definition unary_predicate A := predicate (A::nil).
+
+(** Homogeneous binary relations, equivalent to [relation A]. *)
+
+Definition binary_relation A := predicate (A::A::nil).
+
+(** We can close a predicate by universal or existential quantification. *)
+
+Fixpoint predicate_all (l : list Type) : predicate l -> Prop :=
+  match l with
+    | nil => fun f => f
+    | A :: tl => fun f => forall x : A, predicate_all tl (f x)
+  end.
+
+Fixpoint predicate_exists (l : list Type) : predicate l -> Prop :=
+  match l with
+    | nil => fun f => f
+    | A :: tl => fun f => exists x : A, predicate_exists tl (f x)
+  end.
+
+(** Pointwise extension of a binary operation on [T] to a binary operation
+   on functions whose codomain is [T].
+   For an operator on [Prop] this lifts the operator to a binary operation. *)
+
+Fixpoint pointwise_extension {T : Type} (op : binary_operation T)
+  (l : list Type) : binary_operation (arrows l T) :=
+  match l with
+    | nil => fun R R' => op R R'
+    | A :: tl => fun R R' =>
+      fun x => pointwise_extension op tl (R x) (R' x)
+  end.
+
+(** Pointwise lifting, equivalent to doing [pointwise_extension] and closing using [predicate_all]. *)
+
+Fixpoint pointwise_lifting (op : binary_relation Prop)  (l : list Type) : binary_relation (predicate l) :=
+  match l with
+    | nil => fun R R' => op R R'
+    | A :: tl => fun R R' =>
+      forall x, pointwise_lifting op tl (R x) (R' x)
+  end.
+
+(** The n-ary equivalence relation, defined by lifting the 0-ary [iff] relation. *)
+
+Definition predicate_equivalence {l : list Type} : binary_relation (predicate l) :=
+  pointwise_lifting iff l.
+
+(** The n-ary implication relation, defined by lifting the 0-ary [impl] relation. *)
+
+Definition predicate_implication {l : list Type} :=
+  pointwise_lifting impl l.
+
+(** Notations for pointwise equivalence and implication of predicates. *)
+
+Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope.
+Infix "-∙>" := predicate_implication (at level 70, right associativity) : predicate_scope.
+
+Open Local Scope predicate_scope.
+
+(** The pointwise liftings of conjunction and disjunctions.
+   Note that these are [binary_operation]s, building new relations out of old ones. *)
+
+Definition predicate_intersection := pointwise_extension and.
+Definition predicate_union := pointwise_extension or.
+
+Infix "/∙\" := predicate_intersection (at level 80, right associativity) : predicate_scope.
+Infix "\∙/" := predicate_union (at level 85, right associativity) : predicate_scope.
+
+(** The always [True] and always [False] predicates. *)
+
+Fixpoint true_predicate {l : list Type} : predicate l :=
+  match l with
+    | nil => True
+    | A :: tl => fun _ => @true_predicate tl
+  end.
+
+Fixpoint false_predicate {l : list Type} : predicate l :=
+  match l with
+    | nil => False
+    | A :: tl => fun _ => @false_predicate tl
+  end.
+
+Notation "∙⊤∙" := true_predicate : predicate_scope.
+Notation "∙⊥∙" := false_predicate : predicate_scope.
+
+(** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *)
+
+Program Instance predicate_equivalence_equivalence : Equivalence (@predicate_equivalence l).
+  Next Obligation.
+    induction l ; firstorder.
+  Qed.
+  Next Obligation.
+    induction l ; firstorder.
+  Qed.
+  Next Obligation.
+    fold pointwise_lifting.
+    induction l. firstorder.
+    intros. simpl in *. pose (IHl (x x0) (y x0) (z x0)).
+    firstorder.
+  Qed.
+
+Program Instance predicate_implication_preorder :
+  PreOrder (@predicate_implication l).
+  Next Obligation.
+    induction l ; firstorder.
+  Qed.
+  Next Obligation.
+    induction l. firstorder.
+    unfold predicate_implication in *. simpl in *.
+    intro. pose (IHl (x x0) (y x0) (z x0)). firstorder.
+  Qed.
+
+(** We define the various operations which define the algebra on binary relations,
+   from the general ones. *)
+
+Definition relation_equivalence {A : Type} : relation (relation A) :=
+  @predicate_equivalence (_::_::nil).
+
+Class subrelation {A:Type} (R R' : relation A) : Prop :=
+  is_subrelation : @predicate_implication (A::A::nil) R R'.
+
+Implicit Arguments subrelation [[A]].
+
+Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A :=
+  @predicate_intersection (A::A::nil) R R'.
+
+Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A :=
+  @predicate_union (A::A::nil) R R'.
+
+(** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
+
+Set Automatic Introduction.
+
+Instance relation_equivalence_equivalence (A : Type) :
+  Equivalence (@relation_equivalence A).
+Proof. exact (@predicate_equivalence_equivalence (A::A::nil)). Qed.
+
+Instance relation_implication_preorder A : PreOrder (@subrelation A).
+Proof. exact (@predicate_implication_preorder (A::A::nil)). Qed.
+
+(** *** Partial Order.
+   A partial order is a preorder which is additionally antisymmetric.
+   We give an equivalent definition, up-to an equivalence relation
+   on the carrier. *)
+
+Class PartialOrder {A} eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
+  partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)).
+
+(** The equivalence proof is sufficient for proving that [R] must be a morphism
+   for equivalence (see Morphisms).
+   It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *)
+
+Instance partial_order_antisym `(PartialOrder A eqA R) : ! Antisymmetric A eqA R.
+Proof with auto.
+  reduce_goal.
+  pose proof partial_order_equivalence as poe. do 3 red in poe.
+  apply <- poe. firstorder.
+Qed.
+
+(** The partial order defined by subrelation and relation equivalence. *)
+
+Program Instance subrelation_partial_order :
+  ! PartialOrder (relation A) relation_equivalence subrelation.
+
+  Next Obligation.
+  Proof.
+    unfold relation_equivalence in *. firstorder.
+  Qed.
+
+Typeclasses Opaque arrows predicate_implication predicate_equivalence
+  relation_equivalence pointwise_lifting.
+
+(** Rewrite relation on a given support: declares a relation as a rewrite
+   relation for use by the generalized rewriting tactic.
+   It helps choosing if a rewrite should be handled
+   by the generalized or the regular rewriting tactic using leibniz equality.
+   Users can declare an [RewriteRelation A RA] anywhere to declare default
+   relations. This is also done automatically by the [Declare Relation A RA]
+   commands. *)
+
+Class RewriteRelation {A : Type} (RA : relation A).
+
+Instance: RewriteRelation impl.
+Instance: RewriteRelation iff.
+Instance: RewriteRelation (@relation_equivalence A).
+
+(** Any [Equivalence] declared in the context is automatically considered
+   a rewrite relation. *)
+
+Instance equivalence_rewrite_relation `(Equivalence A eqA) : RewriteRelation eqA.
+
+(** Strict Order *)
+
+Class StrictOrder {A : Type} (R : relation A) := {
+  StrictOrder_Irreflexive :> Irreflexive R ;
+  StrictOrder_Transitive :> Transitive R
+}.
+
+Instance StrictOrder_Asymmetric `(StrictOrder A R) : Asymmetric R.
+Proof. firstorder. Qed.
+
+(** Inversing a [StrictOrder] gives another [StrictOrder] *)
+
+Lemma StrictOrder_inverse `(StrictOrder A R) : StrictOrder (inverse R).
+Proof. firstorder. Qed.
+
+(** Same for [PartialOrder]. *)
+
+Lemma PreOrder_inverse `(PreOrder A R) : PreOrder (inverse R).
+Proof. firstorder. Qed.
+
+Hint Extern 3 (StrictOrder (inverse _)) => class_apply StrictOrder_inverse : typeclass_instances.
+Hint Extern 3 (PreOrder (inverse _)) => class_apply PreOrder_inverse : typeclass_instances.
+
+Lemma PartialOrder_inverse `(PartialOrder A eqA R) : PartialOrder eqA (inverse R).
+Proof. firstorder. Qed.
+
+Hint Extern 3 (PartialOrder (inverse _)) => class_apply PartialOrder_inverse : typeclass_instances.
+
+---tokens---
+'(*'          Comment
+' -'          Comment
+'*'           Comment
+'- coding: utf-8 -' Comment
+'*'           Comment
+'- '          Comment
+'*)'          Comment
+'\n'          Text
+
+'(*'          Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*)'          Comment
+'\n'          Text
+
+'(*'          Comment
+'  v      '   Comment
+'*'           Comment
+'   The Coq Proof Assistant  /  The Coq Development Team     ' Comment
+'*)'          Comment
+'\n'          Text
+
+'(*'          Comment
+' <O___,, '   Comment
+'*'           Comment
+'   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     ' Comment
+'*)'          Comment
+'\n'          Text
+
+'(*'          Comment
+'   \\VV/  '  Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*)'          Comment
+'\n'          Text
+
+'(*'          Comment
+'    //   '   Comment
+'*'           Comment
+'      This file is distributed under the terms of the       ' Comment
+'*)'          Comment
+'\n'          Text
+
+'(*'          Comment
+'         '   Comment
+'*'           Comment
+'       GNU Lesser General Public License Version 2.1        ' Comment
+'*)'          Comment
+'\n'          Text
+
+'(*'          Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+'*)'          Comment
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' '           Comment
+'*'           Comment
+'  Typeclass-based relations, tactics and standard instances\n\n   This is the basic theory needed to formalize morphisms and setoids.\n\n   Author: Matthieu Sozeau\n   Institution: LRI, CNRS UMR 8623 - University Paris Sud\n' Comment
+
+'*)'          Comment
+'\n\n'        Text
+
+'(*'          Comment
+' $Id: RelationClasses.v 14641 2011-11-06 11:59:10Z herbelin $ ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Require'     Keyword.Namespace
+' '           Text
+'Export'      Keyword.Namespace
+' '           Text
+'Coq'         Name
+'.'           Operator
+'Classes'     Name
+'.'           Operator
+'Init'        Name
+'.'           Operator
+'\n'          Text
+
+'Require'     Keyword.Namespace
+' '           Text
+'Import'      Keyword.Namespace
+' '           Text
+'Coq'         Name
+'.'           Operator
+'Program'     Name
+'.'           Operator
+'Basics'      Name
+'.'           Operator
+'\n'          Text
+
+'Require'     Keyword.Namespace
+' '           Text
+'Import'      Keyword.Namespace
+' '           Text
+'Coq'         Name
+'.'           Operator
+'Program'     Name
+'.'           Operator
+'Tactics'     Name
+'.'           Operator
+'\n'          Text
+
+'Require'     Keyword.Namespace
+' '           Text
+'Import'      Keyword.Namespace
+' '           Text
+'Coq'         Name
+'.'           Operator
+'Relations'   Name
+'.'           Operator
+'Relation_Definitions' Name
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' We allow to unfold the [relation] definition while doing morphism search. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Notation'    Keyword.Namespace
+' '           Text
+'inverse'     Name
+' '           Text
+'R'           Name
+' '           Text
+':='          Operator
+' '           Text
+'('           Operator
+'flip'        Name
+' '           Text
+'('           Operator
+'R'           Name
+':'           Operator
+'relation'    Name
+' '           Text
+'_'           Operator
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'_'           Operator
+')'           Operator
+'.'           Operator
+'\n\n'        Text
+
+'Definition'  Keyword.Namespace
+' '           Text
+'complement'  Name
+' '           Text
+'{'           Operator
+'A'           Name
+'}'           Operator
+' '           Text
+'('           Operator
+'R'           Name
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+' '           Text
+':='          Operator
+' '           Text
+'fun'         Keyword
+' '           Text
+'x'           Name
+' '           Text
+'y'           Name
+' '           Text
+'=>'          Operator
+' '           Text
+'R'           Name
+' '           Text
+'x'           Name
+' '           Text
+'y'           Name
+' '           Text
+'->'          Operator
+' '           Text
+'False'       Name
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' Opaque for proof-search. ' Comment
+'*)'          Comment
+'\n'          Text
+
+'Typeclasses' Name
+' '           Text
+'Opaque'      Name
+' '           Text
+'complement'  Name
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' These are convertible. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Lemma'       Keyword.Namespace
+' '           Text
+'complement_inverse' Name
+' '           Text
+':'           Operator
+' '           Text
+'forall'      Keyword
+' '           Text
+'A'           Name
+' '           Text
+'('           Operator
+'R'           Name
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+','           Operator
+' '           Text
+'complement'  Name
+' '           Text
+'('           Operator
+'inverse'     Name
+' '           Text
+'R'           Name
+')'           Operator
+' '           Text
+'='           Operator
+' '           Text
+'inverse'     Name
+' '           Text
+'('           Operator
+'complement'  Name
+' '           Text
+'R'           Name
+')'           Operator
+'.'           Operator
+'\n'          Text
+
+'Proof'       Keyword.Namespace
+'.'           Operator
+' '           Text
+'reflexivity' Keyword.Pseudo
+'.'           Operator
+' '           Text
+'Qed'         Keyword.Namespace
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' We rebind relations in separate classes to be able to overload each proof. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Set'         Keyword.Namespace
+' '           Text
+'Implicit'    Keyword.Namespace
+' '           Text
+'Arguments'   Keyword.Namespace
+'.'           Operator
+'\n'          Text
+
+'Unset'       Keyword.Namespace
+' '           Text
+'Strict'      Keyword.Namespace
+' '           Text
+'Implicit'    Keyword.Namespace
+'.'           Operator
+'\n\n'        Text
+
+'Class'       Keyword.Namespace
+' '           Text
+'Reflexive'   Name
+' '           Text
+'{'           Operator
+'A'           Name
+'}'           Operator
+' '           Text
+'('           Operator
+'R'           Name
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+':='          Operator
+'\n  '        Text
+'reflexivity' Keyword.Pseudo
+' '           Text
+':'           Operator
+' '           Text
+'forall'      Keyword
+' '           Text
+'x'           Name
+','           Operator
+' '           Text
+'R'           Name
+' '           Text
+'x'           Name
+' '           Text
+'x'           Name
+'.'           Operator
+'\n\n'        Text
+
+'Class'       Keyword.Namespace
+' '           Text
+'Irreflexive' Name
+' '           Text
+'{'           Operator
+'A'           Name
+'}'           Operator
+' '           Text
+'('           Operator
+'R'           Name
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+':='          Operator
+'\n  '        Text
+'irreflexivity' Name
+' '           Text
+':'           Operator
+' '           Text
+'Reflexive'   Name
+' '           Text
+'('           Operator
+'complement'  Name
+' '           Text
+'R'           Name
+')'           Operator
+'.'           Operator
+'\n\n'        Text
+
+'Hint'        Keyword.Namespace
+' '           Text
+'Extern'      Name
+' '           Text
+'1'           Literal.Number.Integer
+' '           Text
+'('           Operator
+'Reflexive'   Name
+' '           Text
+'('           Operator
+'complement'  Name
+' '           Text
+'_'           Operator
+')'           Operator
+')'           Operator
+' '           Text
+'=>'          Operator
+' '           Text
+'class_apply' Name
+' '           Text
+'@'           Operator
+'irreflexivity' Name
+' '           Text
+':'           Operator
+' '           Text
+'typeclass_instances' Name
+'.'           Operator
+'\n\n'        Text
+
+'Class'       Keyword.Namespace
+' '           Text
+'Symmetric'   Name
+' '           Text
+'{'           Operator
+'A'           Name
+'}'           Operator
+' '           Text
+'('           Operator
+'R'           Name
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+':='          Operator
+'\n  '        Text
+'symmetry'    Keyword
+' '           Text
+':'           Operator
+' '           Text
+'forall'      Keyword
+' '           Text
+'x'           Name
+' '           Text
+'y'           Name
+','           Operator
+' '           Text
+'R'           Name
+' '           Text
+'x'           Name
+' '           Text
+'y'           Name
+' '           Text
+'->'          Operator
+' '           Text
+'R'           Name
+' '           Text
+'y'           Name
+' '           Text
+'x'           Name
+'.'           Operator
+'\n\n'        Text
+
+'Class'       Keyword.Namespace
+' '           Text
+'Asymmetric'  Name
+' '           Text
+'{'           Operator
+'A'           Name
+'}'           Operator
+' '           Text
+'('           Operator
+'R'           Name
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+':='          Operator
+'\n  '        Text
+'asymmetry'   Name
+' '           Text
+':'           Operator
+' '           Text
+'forall'      Keyword
+' '           Text
+'x'           Name
+' '           Text
+'y'           Name
+','           Operator
+' '           Text
+'R'           Name
+' '           Text
+'x'           Name
+' '           Text
+'y'           Name
+' '           Text
+'->'          Operator
+' '           Text
+'R'           Name
+' '           Text
+'y'           Name
+' '           Text
+'x'           Name
+' '           Text
+'->'          Operator
+' '           Text
+'False'       Name
+'.'           Operator
+'\n\n'        Text
+
+'Class'       Keyword.Namespace
+' '           Text
+'Transitive'  Name
+' '           Text
+'{'           Operator
+'A'           Name
+'}'           Operator
+' '           Text
+'('           Operator
+'R'           Name
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+':='          Operator
+'\n  '        Text
+'transitivity' Keyword
+' '           Text
+':'           Operator
+' '           Text
+'forall'      Keyword
+' '           Text
+'x'           Name
+' '           Text
+'y'           Name
+' '           Text
+'z'           Name
+','           Operator
+' '           Text
+'R'           Name
+' '           Text
+'x'           Name
+' '           Text
+'y'           Name
+' '           Text
+'->'          Operator
+' '           Text
+'R'           Name
+' '           Text
+'y'           Name
+' '           Text
+'z'           Name
+' '           Text
+'->'          Operator
+' '           Text
+'R'           Name
+' '           Text
+'x'           Name
+' '           Text
+'z'           Name
+'.'           Operator
+'\n\n'        Text
+
+'Hint'        Keyword.Namespace
+' '           Text
+'Resolve'     Keyword.Namespace
+' '           Text
+'@'           Operator
+'irreflexivity' Name
+' '           Text
+':'           Operator
+' '           Text
+'ord'         Name
+'.'           Operator
+'\n\n'        Text
+
+'Unset'       Keyword.Namespace
+' '           Text
+'Implicit'    Keyword.Namespace
+' '           Text
+'Arguments'   Keyword.Namespace
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' A HintDb for relations. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Ltac'        Keyword.Namespace
+' '           Text
+'solve_relation' Name
+' '           Text
+':='          Operator
+'\n  '        Text
+'match'       Keyword
+' '           Text
+'goal'        Name
+' '           Text
+'with'        Keyword
+'\n  '        Text
+'|'           Operator
+' '           Text
+'['           Operator
+' '           Text
+'|'           Operator
+'-'           Operator
+' '           Text
+'?'           Operator
+'R'           Name
+' '           Text
+'?'           Operator
+'x'           Name
+' '           Text
+'?'           Operator
+'x'           Name
+' '           Text
+']'           Operator
+' '           Text
+'=>'          Operator
+' '           Text
+'reflexivity' Keyword.Pseudo
+'\n  '        Text
+'|'           Operator
+' '           Text
+'['           Operator
+' '           Text
+'H'           Name
+' '           Text
+':'           Operator
+' '           Text
+'?'           Operator
+'R'           Name
+' '           Text
+'?'           Operator
+'x'           Name
+' '           Text
+'?'           Operator
+'y'           Name
+' '           Text
+'|'           Operator
+'-'           Operator
+' '           Text
+'?'           Operator
+'R'           Name
+' '           Text
+'?'           Operator
+'y'           Name
+' '           Text
+'?'           Operator
+'x'           Name
+' '           Text
+']'           Operator
+' '           Text
+'=>'          Operator
+' '           Text
+'symmetry'    Keyword
+' '           Text
+';'           Operator
+' '           Text
+'exact'       Keyword.Pseudo
+' '           Text
+'H'           Name
+'\n  '        Text
+'end'         Keyword
+'.'           Operator
+'\n\n'        Text
+
+'Hint'        Keyword.Namespace
+' '           Text
+'Extern'      Name
+' '           Text
+'4'           Literal.Number.Integer
+' '           Text
+'=>'          Operator
+' '           Text
+'solve_relation' Name
+' '           Text
+':'           Operator
+' '           Text
+'relations'   Name
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' We can already dualize all these properties. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Generalizable' Name
+' '           Text
+'Variables'   Keyword.Namespace
+' '           Text
+'A'           Name
+' '           Text
+'B'           Name
+' '           Text
+'C'           Name
+' '           Text
+'D'           Name
+' '           Text
+'R'           Name
+' '           Text
+'S'           Name
+' '           Text
+'T'           Name
+' '           Text
+'U'           Name
+' '           Text
+'l'           Name
+' '           Text
+'eqA'         Name
+' '           Text
+'eqB'         Name
+' '           Text
+'eqC'         Name
+' '           Text
+'eqD'         Name
+'.'           Operator
+'\n\n'        Text
+
+'Lemma'       Keyword.Namespace
+' '           Text
+'flip_Reflexive' Name
+' '           Text
+'`'           Operator
+'{'           Operator
+'Reflexive'   Name
+' '           Text
+'A'           Name
+' '           Text
+'R'           Name
+'}'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'Reflexive'   Name
+' '           Text
+'('           Operator
+'flip'        Name
+' '           Text
+'R'           Name
+')'           Operator
+'.'           Operator
+'\n'          Text
+
+'Proof'       Keyword.Namespace
+'.'           Operator
+' '           Text
+'tauto'       Keyword
+'.'           Operator
+' '           Text
+'Qed'         Keyword.Namespace
+'.'           Operator
+'\n\n'        Text
+
+'Hint'        Keyword.Namespace
+' '           Text
+'Extern'      Name
+' '           Text
+'3'           Literal.Number.Integer
+' '           Text
+'('           Operator
+'Reflexive'   Name
+' '           Text
+'('           Operator
+'flip'        Name
+' '           Text
+'_'           Operator
+')'           Operator
+')'           Operator
+' '           Text
+'=>'          Operator
+' '           Text
+'apply'       Keyword
+' '           Text
+'flip_Reflexive' Name
+' '           Text
+':'           Operator
+' '           Text
+'typeclass_instances' Name
+'.'           Operator
+'\n\n'        Text
+
+'Program'     Name
+' '           Text
+'Definition'  Keyword.Namespace
+' '           Text
+'flip_Irreflexive' Name
+' '           Text
+'`'           Operator
+'('           Operator
+'Irreflexive' Name
+' '           Text
+'A'           Name
+' '           Text
+'R'           Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'Irreflexive' Name
+' '           Text
+'('           Operator
+'flip'        Name
+' '           Text
+'R'           Name
+')'           Operator
+' '           Text
+':='          Operator
+'\n  '        Text
+'irreflexivity' Name
+' '           Text
+'('           Operator
+'R'           Name
+':='          Operator
+'R'           Name
+')'           Operator
+'.'           Operator
+'\n\n'        Text
+
+'Program'     Name
+' '           Text
+'Definition'  Keyword.Namespace
+' '           Text
+'flip_Symmetric' Name
+' '           Text
+'`'           Operator
+'('           Operator
+'Symmetric'   Name
+' '           Text
+'A'           Name
+' '           Text
+'R'           Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'Symmetric'   Name
+' '           Text
+'('           Operator
+'flip'        Name
+' '           Text
+'R'           Name
+')'           Operator
+' '           Text
+':='          Operator
+'\n  '        Text
+'fun'         Keyword
+' '           Text
+'x'           Name
+' '           Text
+'y'           Name
+' '           Text
+'H'           Name
+' '           Text
+'=>'          Operator
+' '           Text
+'symmetry'    Keyword
+' '           Text
+'('           Operator
+'R'           Name
+':='          Operator
+'R'           Name
+')'           Operator
+' '           Text
+'H'           Name
+'.'           Operator
+'\n\n'        Text
+
+'Program'     Name
+' '           Text
+'Definition'  Keyword.Namespace
+' '           Text
+'flip_Asymmetric' Name
+' '           Text
+'`'           Operator
+'('           Operator
+'Asymmetric'  Name
+' '           Text
+'A'           Name
+' '           Text
+'R'           Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'Asymmetric'  Name
+' '           Text
+'('           Operator
+'flip'        Name
+' '           Text
+'R'           Name
+')'           Operator
+' '           Text
+':='          Operator
+'\n  '        Text
+'fun'         Keyword
+' '           Text
+'x'           Name
+' '           Text
+'y'           Name
+' '           Text
+'H'           Name
+' '           Text
+"H'"          Name
+' '           Text
+'=>'          Operator
+' '           Text
+'asymmetry'   Name
+' '           Text
+'('           Operator
+'R'           Name
+':='          Operator
+'R'           Name
+')'           Operator
+' '           Text
+'H'           Name
+' '           Text
+"H'"          Name
+'.'           Operator
+'\n\n'        Text
+
+'Program'     Name
+' '           Text
+'Definition'  Keyword.Namespace
+' '           Text
+'flip_Transitive' Name
+' '           Text
+'`'           Operator
+'('           Operator
+'Transitive'  Name
+' '           Text
+'A'           Name
+' '           Text
+'R'           Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'Transitive'  Name
+' '           Text
+'('           Operator
+'flip'        Name
+' '           Text
+'R'           Name
+')'           Operator
+' '           Text
+':='          Operator
+'\n  '        Text
+'fun'         Keyword
+' '           Text
+'x'           Name
+' '           Text
+'y'           Name
+' '           Text
+'z'           Name
+' '           Text
+'H'           Name
+' '           Text
+"H'"          Name
+' '           Text
+'=>'          Operator
+' '           Text
+'transitivity' Keyword
+' '           Text
+'('           Operator
+'R'           Name
+':='          Operator
+'R'           Name
+')'           Operator
+' '           Text
+"H'"          Name
+' '           Text
+'H'           Name
+'.'           Operator
+'\n\n'        Text
+
+'Hint'        Keyword.Namespace
+' '           Text
+'Extern'      Name
+' '           Text
+'3'           Literal.Number.Integer
+' '           Text
+'('           Operator
+'Irreflexive' Name
+' '           Text
+'('           Operator
+'flip'        Name
+' '           Text
+'_'           Operator
+')'           Operator
+')'           Operator
+' '           Text
+'=>'          Operator
+' '           Text
+'class_apply' Name
+' '           Text
+'flip_Irreflexive' Name
+' '           Text
+':'           Operator
+' '           Text
+'typeclass_instances' Name
+'.'           Operator
+'\n'          Text
+
+'Hint'        Keyword.Namespace
+' '           Text
+'Extern'      Name
+' '           Text
+'3'           Literal.Number.Integer
+' '           Text
+'('           Operator
+'Symmetric'   Name
+' '           Text
+'('           Operator
+'flip'        Name
+' '           Text
+'_'           Operator
+')'           Operator
+')'           Operator
+' '           Text
+'=>'          Operator
+' '           Text
+'class_apply' Name
+' '           Text
+'flip_Symmetric' Name
+' '           Text
+':'           Operator
+' '           Text
+'typeclass_instances' Name
+'.'           Operator
+'\n'          Text
+
+'Hint'        Keyword.Namespace
+' '           Text
+'Extern'      Name
+' '           Text
+'3'           Literal.Number.Integer
+' '           Text
+'('           Operator
+'Asymmetric'  Name
+' '           Text
+'('           Operator
+'flip'        Name
+' '           Text
+'_'           Operator
+')'           Operator
+')'           Operator
+' '           Text
+'=>'          Operator
+' '           Text
+'class_apply' Name
+' '           Text
+'flip_Asymmetric' Name
+' '           Text
+':'           Operator
+' '           Text
+'typeclass_instances' Name
+'.'           Operator
+'\n'          Text
+
+'Hint'        Keyword.Namespace
+' '           Text
+'Extern'      Name
+' '           Text
+'3'           Literal.Number.Integer
+' '           Text
+'('           Operator
+'Transitive'  Name
+' '           Text
+'('           Operator
+'flip'        Name
+' '           Text
+'_'           Operator
+')'           Operator
+')'           Operator
+' '           Text
+'=>'          Operator
+' '           Text
+'class_apply' Name
+' '           Text
+'flip_Transitive' Name
+' '           Text
+':'           Operator
+' '           Text
+'typeclass_instances' Name
+'.'           Operator
+'\n\n'        Text
+
+'Definition'  Keyword.Namespace
+' '           Text
+'Reflexive_complement_Irreflexive' Name
+' '           Text
+'`'           Operator
+'('           Operator
+'Reflexive'   Name
+' '           Text
+'A'           Name
+' '           Text
+'('           Operator
+'R'           Name
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+')'           Operator
+'\n   '       Text
+':'           Operator
+' '           Text
+'Irreflexive' Name
+' '           Text
+'('           Operator
+'complement'  Name
+' '           Text
+'R'           Name
+')'           Operator
+'.'           Operator
+'\n'          Text
+
+'Proof'       Keyword.Namespace
+'.'           Operator
+' '           Text
+'firstorder'  Name
+'.'           Operator
+' '           Text
+'Qed'         Keyword.Namespace
+'.'           Operator
+'\n\n'        Text
+
+'Definition'  Keyword.Namespace
+' '           Text
+'complement_Symmetric' Name
+' '           Text
+'`'           Operator
+'('           Operator
+'Symmetric'   Name
+' '           Text
+'A'           Name
+' '           Text
+'('           Operator
+'R'           Name
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'Symmetric'   Name
+' '           Text
+'('           Operator
+'complement'  Name
+' '           Text
+'R'           Name
+')'           Operator
+'.'           Operator
+'\n'          Text
+
+'Proof'       Keyword.Namespace
+'.'           Operator
+' '           Text
+'firstorder'  Name
+'.'           Operator
+' '           Text
+'Qed'         Keyword.Namespace
+'.'           Operator
+'\n\n'        Text
+
+'Hint'        Keyword.Namespace
+' '           Text
+'Extern'      Name
+' '           Text
+'3'           Literal.Number.Integer
+' '           Text
+'('           Operator
+'Symmetric'   Name
+' '           Text
+'('           Operator
+'complement'  Name
+' '           Text
+'_'           Operator
+')'           Operator
+')'           Operator
+' '           Text
+'=>'          Operator
+' '           Text
+'class_apply' Name
+' '           Text
+'complement_Symmetric' Name
+' '           Text
+':'           Operator
+' '           Text
+'typeclass_instances' Name
+'.'           Operator
+'\n'          Text
+
+'Hint'        Keyword.Namespace
+' '           Text
+'Extern'      Name
+' '           Text
+'3'           Literal.Number.Integer
+' '           Text
+'('           Operator
+'Irreflexive' Name
+' '           Text
+'('           Operator
+'complement'  Name
+' '           Text
+'_'           Operator
+')'           Operator
+')'           Operator
+' '           Text
+'=>'          Operator
+' '           Text
+'class_apply' Name
+' '           Text
+'Reflexive_complement_Irreflexive' Name
+' '           Text
+':'           Operator
+' '           Text
+'typeclass_instances' Name
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' '           Comment
+'*'           Comment
+' Standard instances. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Ltac'        Keyword.Namespace
+' '           Text
+'reduce_hyp'  Name
+' '           Text
+'H'           Name
+' '           Text
+':='          Operator
+'\n  '        Text
+'match'       Keyword
+' '           Text
+'type'        Name
+' '           Text
+'of'          Keyword
+' '           Text
+'H'           Name
+' '           Text
+'with'        Keyword
+'\n    '      Text
+'|'           Operator
+' '           Text
+'context'     Name
+' '           Text
+'['           Operator
+' '           Text
+'_'           Operator
+' '           Text
+'<->'         Operator
+' '           Text
+'_'           Operator
+' '           Text
+']'           Operator
+' '           Text
+'=>'          Operator
+' '           Text
+'fail'        Name
+' '           Text
+'1'           Literal.Number.Integer
+'\n    '      Text
+'|'           Operator
+' '           Text
+'_'           Operator
+' '           Text
+'=>'          Operator
+' '           Text
+'red'         Keyword
+' '           Text
+'in'          Keyword
+' '           Text
+'H'           Name
+' '           Text
+';'           Operator
+' '           Text
+'try'         Keyword.Reserved
+' '           Text
+'reduce_hyp'  Name
+' '           Text
+'H'           Name
+'\n  '        Text
+'end'         Keyword
+'.'           Operator
+'\n\n'        Text
+
+'Ltac'        Keyword.Namespace
+' '           Text
+'reduce_goal' Name
+' '           Text
+':='          Operator
+'\n  '        Text
+'match'       Keyword
+' '           Text
+'goal'        Name
+' '           Text
+'with'        Keyword
+'\n    '      Text
+'|'           Operator
+' '           Text
+'['           Operator
+' '           Text
+'|'           Operator
+'-'           Operator
+' '           Text
+'_'           Operator
+' '           Text
+'<->'         Operator
+' '           Text
+'_'           Operator
+' '           Text
+']'           Operator
+' '           Text
+'=>'          Operator
+' '           Text
+'fail'        Name
+' '           Text
+'1'           Literal.Number.Integer
+'\n    '      Text
+'|'           Operator
+' '           Text
+'_'           Operator
+' '           Text
+'=>'          Operator
+' '           Text
+'red'         Keyword
+' '           Text
+';'           Operator
+' '           Text
+'intros'      Keyword
+' '           Text
+';'           Operator
+' '           Text
+'try'         Keyword.Reserved
+' '           Text
+'reduce_goal' Name
+'\n  '        Text
+'end'         Keyword
+'.'           Operator
+'\n\n'        Text
+
+'Tactic'      Keyword.Namespace
+' '           Text
+'Notation'    Keyword.Namespace
+' '           Text
+'"'           Literal.String.Double
+'reduce'      Literal.String.Double
+'"'           Literal.String.Double
+' '           Text
+'"'           Literal.String.Double
+'in'          Literal.String.Double
+'"'           Literal.String.Double
+' '           Text
+'hyp'         Name
+'('           Operator
+'Hid'         Name
+')'           Operator
+' '           Text
+':='          Operator
+' '           Text
+'reduce_hyp'  Name
+' '           Text
+'Hid'         Name
+'.'           Operator
+'\n\n'        Text
+
+'Ltac'        Keyword.Namespace
+' '           Text
+'reduce'      Name
+' '           Text
+':='          Operator
+' '           Text
+'reduce_goal' Name
+'.'           Operator
+'\n\n'        Text
+
+'Tactic'      Keyword.Namespace
+' '           Text
+'Notation'    Keyword.Namespace
+' '           Text
+'"'           Literal.String.Double
+'apply'       Literal.String.Double
+'"'           Literal.String.Double
+' '           Text
+'"'           Literal.String.Double
+'*'           Literal.String.Double
+'"'           Literal.String.Double
+' '           Text
+'constr'      Name
+'('           Operator
+'t'           Name
+')'           Operator
+' '           Text
+':='          Operator
+'\n  '        Text
+'first'       Keyword.Reserved
+' '           Text
+'['           Operator
+' '           Text
+'refine'      Keyword
+' '           Text
+'t'           Name
+' '           Text
+'|'           Operator
+' '           Text
+'refine'      Keyword
+' '           Text
+'('           Operator
+'t'           Name
+' '           Text
+'_'           Operator
+')'           Operator
+' '           Text
+'|'           Operator
+' '           Text
+'refine'      Keyword
+' '           Text
+'('           Operator
+'t'           Name
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+')'           Operator
+' '           Text
+'|'           Operator
+' '           Text
+'refine'      Keyword
+' '           Text
+'('           Operator
+'t'           Name
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+')'           Operator
+' '           Text
+'|'           Operator
+' '           Text
+'refine'      Keyword
+' '           Text
+'('           Operator
+'t'           Name
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+')'           Operator
+' '           Text
+'|'           Operator
+'\n    '      Text
+'refine'      Keyword
+' '           Text
+'('           Operator
+'t'           Name
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+')'           Operator
+' '           Text
+'|'           Operator
+' '           Text
+'refine'      Keyword
+' '           Text
+'('           Operator
+'t'           Name
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+')'           Operator
+' '           Text
+'|'           Operator
+' '           Text
+'refine'      Keyword
+' '           Text
+'('           Operator
+'t'           Name
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+' '           Text
+'_'           Operator
+')'           Operator
+' '           Text
+']'           Operator
+'.'           Operator
+'\n\n'        Text
+
+'Ltac'        Keyword.Namespace
+' '           Text
+'simpl_relation' Name
+' '           Text
+':='          Operator
+'\n  '        Text
+'unfold'      Keyword
+' '           Text
+'flip'        Name
+','           Operator
+' '           Text
+'impl'        Name
+','           Operator
+' '           Text
+'arrow'       Name
+' '           Text
+';'           Operator
+' '           Text
+'try'         Keyword.Reserved
+' '           Text
+'reduce'      Name
+' '           Text
+';'           Operator
+' '           Text
+'program_simpl' Name
+' '           Text
+';'           Operator
+'\n    '      Text
+'try'         Keyword.Reserved
+' '           Text
+'('           Operator
+' '           Text
+'solve'       Keyword.Pseudo
+' '           Text
+'['           Operator
+' '           Text
+'intuition'   Keyword
+' '           Text
+']'           Operator
+')'           Operator
+'.'           Operator
+'\n\n'        Text
+
+'Local'       Keyword.Namespace
+' '           Text
+'Obligation'  Name
+' '           Text
+'Tactic'      Keyword.Namespace
+' '           Text
+':='          Operator
+' '           Text
+'simpl_relation' Name
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' Logical implication. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Program'     Name
+' '           Text
+'Instance'    Keyword.Namespace
+' '           Text
+'impl_Reflexive' Name
+' '           Text
+':'           Operator
+' '           Text
+'Reflexive'   Name
+' '           Text
+'impl'        Name
+'.'           Operator
+'\n'          Text
+
+'Program'     Name
+' '           Text
+'Instance'    Keyword.Namespace
+' '           Text
+'impl_Transitive' Name
+' '           Text
+':'           Operator
+' '           Text
+'Transitive'  Name
+' '           Text
+'impl'        Name
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' Logical equivalence. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Program'     Name
+' '           Text
+'Instance'    Keyword.Namespace
+' '           Text
+'iff_Reflexive' Name
+' '           Text
+':'           Operator
+' '           Text
+'Reflexive'   Name
+' '           Text
+'iff'         Name
+'.'           Operator
+'\n'          Text
+
+'Program'     Name
+' '           Text
+'Instance'    Keyword.Namespace
+' '           Text
+'iff_Symmetric' Name
+' '           Text
+':'           Operator
+' '           Text
+'Symmetric'   Name
+' '           Text
+'iff'         Name
+'.'           Operator
+'\n'          Text
+
+'Program'     Name
+' '           Text
+'Instance'    Keyword.Namespace
+' '           Text
+'iff_Transitive' Name
+' '           Text
+':'           Operator
+' '           Text
+'Transitive'  Name
+' '           Text
+'iff'         Name
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' Leibniz equality. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Instance'    Keyword.Namespace
+' '           Text
+'eq_Reflexive' Name
+' '           Text
+'{'           Operator
+'A'           Name
+'}'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'Reflexive'   Name
+' '           Text
+'('           Operator
+'@'           Operator
+'eq'          Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+':='          Operator
+' '           Text
+'@'           Operator
+'eq_refl'     Name
+' '           Text
+'A'           Name
+'.'           Operator
+'\n'          Text
+
+'Instance'    Keyword.Namespace
+' '           Text
+'eq_Symmetric' Name
+' '           Text
+'{'           Operator
+'A'           Name
+'}'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'Symmetric'   Name
+' '           Text
+'('           Operator
+'@'           Operator
+'eq'          Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+':='          Operator
+' '           Text
+'@'           Operator
+'eq_sym'      Name
+' '           Text
+'A'           Name
+'.'           Operator
+'\n'          Text
+
+'Instance'    Keyword.Namespace
+' '           Text
+'eq_Transitive' Name
+' '           Text
+'{'           Operator
+'A'           Name
+'}'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'Transitive'  Name
+' '           Text
+'('           Operator
+'@'           Operator
+'eq'          Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+':='          Operator
+' '           Text
+'@'           Operator
+'eq_trans'    Name
+' '           Text
+'A'           Name
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' Various combinations of reflexivity, symmetry and transitivity. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' A [PreOrder] is both Reflexive and Transitive. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Class'       Keyword.Namespace
+' '           Text
+'PreOrder'    Name
+' '           Text
+'{'           Operator
+'A'           Name
+'}'           Operator
+' '           Text
+'('           Operator
+'R'           Name
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'Prop'        Keyword.Type
+' '           Text
+':='          Operator
+' '           Text
+'{'           Operator
+'\n  '        Text
+'PreOrder_Reflexive' Name
+' '           Text
+':>'          Operator
+' '           Text
+'Reflexive'   Name
+' '           Text
+'R'           Name
+' '           Text
+';'           Operator
+'\n  '        Text
+'PreOrder_Transitive' Name
+' '           Text
+':>'          Operator
+' '           Text
+'Transitive'  Name
+' '           Text
+'R'           Name
+' '           Text
+'}'           Operator
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' A partial equivalence relation is Symmetric and Transitive. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Class'       Keyword.Namespace
+' '           Text
+'PER'         Name
+' '           Text
+'{'           Operator
+'A'           Name
+'}'           Operator
+' '           Text
+'('           Operator
+'R'           Name
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'Prop'        Keyword.Type
+' '           Text
+':='          Operator
+' '           Text
+'{'           Operator
+'\n  '        Text
+'PER_Symmetric' Name
+' '           Text
+':>'          Operator
+' '           Text
+'Symmetric'   Name
+' '           Text
+'R'           Name
+' '           Text
+';'           Operator
+'\n  '        Text
+'PER_Transitive' Name
+' '           Text
+':>'          Operator
+' '           Text
+'Transitive'  Name
+' '           Text
+'R'           Name
+' '           Text
+'}'           Operator
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' Equivalence relations. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Class'       Keyword.Namespace
+' '           Text
+'Equivalence' Name
+' '           Text
+'{'           Operator
+'A'           Name
+'}'           Operator
+' '           Text
+'('           Operator
+'R'           Name
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'Prop'        Keyword.Type
+' '           Text
+':='          Operator
+' '           Text
+'{'           Operator
+'\n  '        Text
+'Equivalence_Reflexive' Name
+' '           Text
+':>'          Operator
+' '           Text
+'Reflexive'   Name
+' '           Text
+'R'           Name
+' '           Text
+';'           Operator
+'\n  '        Text
+'Equivalence_Symmetric' Name
+' '           Text
+':>'          Operator
+' '           Text
+'Symmetric'   Name
+' '           Text
+'R'           Name
+' '           Text
+';'           Operator
+'\n  '        Text
+'Equivalence_Transitive' Name
+' '           Text
+':>'          Operator
+' '           Text
+'Transitive'  Name
+' '           Text
+'R'           Name
+' '           Text
+'}'           Operator
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' An Equivalence is a PER plus reflexivity. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Instance'    Keyword.Namespace
+' '           Text
+'Equivalence_PER' Name
+' '           Text
+'`'           Operator
+'('           Operator
+'Equivalence' Name
+' '           Text
+'A'           Name
+' '           Text
+'R'           Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'PER'         Name
+' '           Text
+'R'           Name
+' '           Text
+'|'           Operator
+' '           Text
+'10'          Literal.Number.Integer
+' '           Text
+':='          Operator
+'\n  '        Text
+'{'           Operator
+' '           Text
+'PER_Symmetric' Name
+' '           Text
+':='          Operator
+' '           Text
+'Equivalence_Symmetric' Name
+' '           Text
+';'           Operator
+'\n    '      Text
+'PER_Transitive' Name
+' '           Text
+':='          Operator
+' '           Text
+'Equivalence_Transitive' Name
+' '           Text
+'}'           Operator
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' We can now define antisymmetry w.r.t. an equivalence relation on the carrier. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Class'       Keyword.Namespace
+' '           Text
+'Antisymmetric' Name
+' '           Text
+'A'           Name
+' '           Text
+'eqA'         Name
+' '           Text
+'`'           Operator
+'{'           Operator
+'equ'         Name
+' '           Text
+':'           Operator
+' '           Text
+'Equivalence' Name
+' '           Text
+'A'           Name
+' '           Text
+'eqA'         Name
+'}'           Operator
+' '           Text
+'('           Operator
+'R'           Name
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+':='          Operator
+'\n  '        Text
+'antisymmetry' Name
+' '           Text
+':'           Operator
+' '           Text
+'forall'      Keyword
+' '           Text
+'{'           Operator
+'x'           Name
+' '           Text
+'y'           Name
+'}'           Operator
+','           Operator
+' '           Text
+'R'           Name
+' '           Text
+'x'           Name
+' '           Text
+'y'           Name
+' '           Text
+'->'          Operator
+' '           Text
+'R'           Name
+' '           Text
+'y'           Name
+' '           Text
+'x'           Name
+' '           Text
+'->'          Operator
+' '           Text
+'eqA'         Name
+' '           Text
+'x'           Name
+' '           Text
+'y'           Name
+'.'           Operator
+'\n\n'        Text
+
+'Program'     Name
+' '           Text
+'Definition'  Keyword.Namespace
+' '           Text
+'flip_antiSymmetric' Name
+' '           Text
+'`'           Operator
+'('           Operator
+'Antisymmetric' Name
+' '           Text
+'A'           Name
+' '           Text
+'eqA'         Name
+' '           Text
+'R'           Name
+')'           Operator
+' '           Text
+':'           Operator
+'\n  '        Text
+'Antisymmetric' Name
+' '           Text
+'A'           Name
+' '           Text
+'eqA'         Name
+' '           Text
+'('           Operator
+'flip'        Name
+' '           Text
+'R'           Name
+')'           Operator
+'.'           Operator
+'\n'          Text
+
+'Proof'       Keyword.Namespace
+'.'           Operator
+' '           Text
+'firstorder'  Name
+'.'           Operator
+' '           Text
+'Qed'         Keyword.Namespace
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' Leibinz equality [eq] is an equivalence relation.\n   The instance has low priority as it is always applicable\n   if only the type is constrained. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Program'     Name
+' '           Text
+'Instance'    Keyword.Namespace
+' '           Text
+'eq_equivalence' Name
+' '           Text
+':'           Operator
+' '           Text
+'Equivalence' Name
+' '           Text
+'('           Operator
+'@'           Operator
+'eq'          Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+'|'           Operator
+' '           Text
+'10'          Literal.Number.Integer
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' Logical equivalence [iff] is an equivalence relation. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Program'     Name
+' '           Text
+'Instance'    Keyword.Namespace
+' '           Text
+'iff_equivalence' Name
+' '           Text
+':'           Operator
+' '           Text
+'Equivalence' Name
+' '           Text
+'iff'         Name
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' We now develop a generalization of results on relations for arbitrary predicates.\n   The resulting theory can be applied to homogeneous binary relations but also to\n   arbitrary n-ary predicates. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Local'       Keyword.Namespace
+' '           Text
+'Open'        Keyword.Namespace
+' '           Text
+'Scope'       Keyword.Namespace
+' '           Text
+'list_scope'  Name
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+' Notation " [ ] " := nil : list_scope. ' Comment
+'*)'          Comment
+'\n'          Text
+
+'(*'          Comment
+' Notation " [ x ; .. ; y ] " := ' Comment
+'('           Comment
+'cons x .. '  Comment
+'('           Comment
+'cons y nil'  Comment
+')'           Comment
+' ..'         Comment
+')'           Comment
+' '           Comment
+'('           Comment
+'at level 1'  Comment
+')'           Comment
+' : list_scope. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' A compact representation of non-dependent arities, with the codomain singled-out. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Fixpoint'    Keyword.Namespace
+' '           Text
+'arrows'      Name
+' '           Text
+'('           Operator
+'l'           Name
+' '           Text
+':'           Operator
+' '           Text
+'list'        Name
+' '           Text
+'Type'        Keyword.Type
+')'           Operator
+' '           Text
+'('           Operator
+'r'           Name
+' '           Text
+':'           Operator
+' '           Text
+'Type'        Keyword.Type
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'Type'        Keyword.Type
+' '           Text
+':='          Operator
+'\n  '        Text
+'match'       Keyword
+' '           Text
+'l'           Name
+' '           Text
+'with'        Keyword
+'\n    '      Text
+'|'           Operator
+' '           Text
+'nil'         Name
+' '           Text
+'=>'          Operator
+' '           Text
+'r'           Name
+'\n    '      Text
+'|'           Operator
+' '           Text
+'A'           Name
+' '           Text
+'::'          Operator
+' '           Text
+"l'"          Name
+' '           Text
+'=>'          Operator
+' '           Text
+'A'           Name
+' '           Text
+'->'          Operator
+' '           Text
+'arrows'      Name
+' '           Text
+"l'"          Name
+' '           Text
+'r'           Name
+'\n  '        Text
+'end'         Keyword
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' We can define abbreviations for operation and relation types based on [arrows]. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Definition'  Keyword.Namespace
+' '           Text
+'unary_operation' Name
+' '           Text
+'A'           Name
+' '           Text
+':='          Operator
+' '           Text
+'arrows'      Name
+' '           Text
+'('           Operator
+'A'           Name
+'::'          Operator
+'nil'         Name
+')'           Operator
+' '           Text
+'A'           Name
+'.'           Operator
+'\n'          Text
+
+'Definition'  Keyword.Namespace
+' '           Text
+'binary_operation' Name
+' '           Text
+'A'           Name
+' '           Text
+':='          Operator
+' '           Text
+'arrows'      Name
+' '           Text
+'('           Operator
+'A'           Name
+'::'          Operator
+'A'           Name
+'::'          Operator
+'nil'         Name
+')'           Operator
+' '           Text
+'A'           Name
+'.'           Operator
+'\n'          Text
+
+'Definition'  Keyword.Namespace
+' '           Text
+'ternary_operation' Name
+' '           Text
+'A'           Name
+' '           Text
+':='          Operator
+' '           Text
+'arrows'      Name
+' '           Text
+'('           Operator
+'A'           Name
+'::'          Operator
+'A'           Name
+'::'          Operator
+'A'           Name
+'::'          Operator
+'nil'         Name
+')'           Operator
+' '           Text
+'A'           Name
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' We define n-ary [predicate]s as functions into [Prop]. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Notation'    Keyword.Namespace
+' '           Text
+'predicate'   Name
+' '           Text
+'l'           Name
+' '           Text
+':='          Operator
+' '           Text
+'('           Operator
+'arrows'      Name
+' '           Text
+'l'           Name
+' '           Text
+'Prop'        Keyword.Type
+')'           Operator
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' Unary predicates, or sets. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Definition'  Keyword.Namespace
+' '           Text
+'unary_predicate' Name
+' '           Text
+'A'           Name
+' '           Text
+':='          Operator
+' '           Text
+'predicate'   Name
+' '           Text
+'('           Operator
+'A'           Name
+'::'          Operator
+'nil'         Name
+')'           Operator
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' Homogeneous binary relations, equivalent to [relation A]. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Definition'  Keyword.Namespace
+' '           Text
+'binary_relation' Name
+' '           Text
+'A'           Name
+' '           Text
+':='          Operator
+' '           Text
+'predicate'   Name
+' '           Text
+'('           Operator
+'A'           Name
+'::'          Operator
+'A'           Name
+'::'          Operator
+'nil'         Name
+')'           Operator
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' We can close a predicate by universal or existential quantification. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Fixpoint'    Keyword.Namespace
+' '           Text
+'predicate_all' Name
+' '           Text
+'('           Operator
+'l'           Name
+' '           Text
+':'           Operator
+' '           Text
+'list'        Name
+' '           Text
+'Type'        Keyword.Type
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'predicate'   Name
+' '           Text
+'l'           Name
+' '           Text
+'->'          Operator
+' '           Text
+'Prop'        Keyword.Type
+' '           Text
+':='          Operator
+'\n  '        Text
+'match'       Keyword
+' '           Text
+'l'           Name
+' '           Text
+'with'        Keyword
+'\n    '      Text
+'|'           Operator
+' '           Text
+'nil'         Name
+' '           Text
+'=>'          Operator
+' '           Text
+'fun'         Keyword
+' '           Text
+'f'           Name
+' '           Text
+'=>'          Operator
+' '           Text
+'f'           Name
+'\n    '      Text
+'|'           Operator
+' '           Text
+'A'           Name
+' '           Text
+'::'          Operator
+' '           Text
+'tl'          Name
+' '           Text
+'=>'          Operator
+' '           Text
+'fun'         Keyword
+' '           Text
+'f'           Name
+' '           Text
+'=>'          Operator
+' '           Text
+'forall'      Keyword
+' '           Text
+'x'           Name
+' '           Text
+':'           Operator
+' '           Text
+'A'           Name
+','           Operator
+' '           Text
+'predicate_all' Name
+' '           Text
+'tl'          Name
+' '           Text
+'('           Operator
+'f'           Name
+' '           Text
+'x'           Name
+')'           Operator
+'\n  '        Text
+'end'         Keyword
+'.'           Operator
+'\n\n'        Text
+
+'Fixpoint'    Keyword.Namespace
+' '           Text
+'predicate_exists' Name
+' '           Text
+'('           Operator
+'l'           Name
+' '           Text
+':'           Operator
+' '           Text
+'list'        Name
+' '           Text
+'Type'        Keyword.Type
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'predicate'   Name
+' '           Text
+'l'           Name
+' '           Text
+'->'          Operator
+' '           Text
+'Prop'        Keyword.Type
+' '           Text
+':='          Operator
+'\n  '        Text
+'match'       Keyword
+' '           Text
+'l'           Name
+' '           Text
+'with'        Keyword
+'\n    '      Text
+'|'           Operator
+' '           Text
+'nil'         Name
+' '           Text
+'=>'          Operator
+' '           Text
+'fun'         Keyword
+' '           Text
+'f'           Name
+' '           Text
+'=>'          Operator
+' '           Text
+'f'           Name
+'\n    '      Text
+'|'           Operator
+' '           Text
+'A'           Name
+' '           Text
+'::'          Operator
+' '           Text
+'tl'          Name
+' '           Text
+'=>'          Operator
+' '           Text
+'fun'         Keyword
+' '           Text
+'f'           Name
+' '           Text
+'=>'          Operator
+' '           Text
+'exists'      Keyword
+' '           Text
+'x'           Name
+' '           Text
+':'           Operator
+' '           Text
+'A'           Name
+','           Operator
+' '           Text
+'predicate_exists' Name
+' '           Text
+'tl'          Name
+' '           Text
+'('           Operator
+'f'           Name
+' '           Text
+'x'           Name
+')'           Operator
+'\n  '        Text
+'end'         Keyword
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' Pointwise extension of a binary operation on [T] to a binary operation\n   on functions whose codomain is [T].\n   For an operator on [Prop] this lifts the operator to a binary operation. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Fixpoint'    Keyword.Namespace
+' '           Text
+'pointwise_extension' Name
+' '           Text
+'{'           Operator
+'T'           Name
+' '           Text
+':'           Operator
+' '           Text
+'Type'        Keyword.Type
+'}'           Operator
+' '           Text
+'('           Operator
+'op'          Name
+' '           Text
+':'           Operator
+' '           Text
+'binary_operation' Name
+' '           Text
+'T'           Name
+')'           Operator
+'\n  '        Text
+'('           Operator
+'l'           Name
+' '           Text
+':'           Operator
+' '           Text
+'list'        Name
+' '           Text
+'Type'        Keyword.Type
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'binary_operation' Name
+' '           Text
+'('           Operator
+'arrows'      Name
+' '           Text
+'l'           Name
+' '           Text
+'T'           Name
+')'           Operator
+' '           Text
+':='          Operator
+'\n  '        Text
+'match'       Keyword
+' '           Text
+'l'           Name
+' '           Text
+'with'        Keyword
+'\n    '      Text
+'|'           Operator
+' '           Text
+'nil'         Name
+' '           Text
+'=>'          Operator
+' '           Text
+'fun'         Keyword
+' '           Text
+'R'           Name
+' '           Text
+"R'"          Name
+' '           Text
+'=>'          Operator
+' '           Text
+'op'          Name
+' '           Text
+'R'           Name
+' '           Text
+"R'"          Name
+'\n    '      Text
+'|'           Operator
+' '           Text
+'A'           Name
+' '           Text
+'::'          Operator
+' '           Text
+'tl'          Name
+' '           Text
+'=>'          Operator
+' '           Text
+'fun'         Keyword
+' '           Text
+'R'           Name
+' '           Text
+"R'"          Name
+' '           Text
+'=>'          Operator
+'\n      '    Text
+'fun'         Keyword
+' '           Text
+'x'           Name
+' '           Text
+'=>'          Operator
+' '           Text
+'pointwise_extension' Name
+' '           Text
+'op'          Name
+' '           Text
+'tl'          Name
+' '           Text
+'('           Operator
+'R'           Name
+' '           Text
+'x'           Name
+')'           Operator
+' '           Text
+'('           Operator
+"R'"          Name
+' '           Text
+'x'           Name
+')'           Operator
+'\n  '        Text
+'end'         Keyword
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' Pointwise lifting, equivalent to doing [pointwise_extension] and closing using [predicate_all]. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Fixpoint'    Keyword.Namespace
+' '           Text
+'pointwise_lifting' Name
+' '           Text
+'('           Operator
+'op'          Name
+' '           Text
+':'           Operator
+' '           Text
+'binary_relation' Name
+' '           Text
+'Prop'        Keyword.Type
+')'           Operator
+'  '          Text
+'('           Operator
+'l'           Name
+' '           Text
+':'           Operator
+' '           Text
+'list'        Name
+' '           Text
+'Type'        Keyword.Type
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'binary_relation' Name
+' '           Text
+'('           Operator
+'predicate'   Name
+' '           Text
+'l'           Name
+')'           Operator
+' '           Text
+':='          Operator
+'\n  '        Text
+'match'       Keyword
+' '           Text
+'l'           Name
+' '           Text
+'with'        Keyword
+'\n    '      Text
+'|'           Operator
+' '           Text
+'nil'         Name
+' '           Text
+'=>'          Operator
+' '           Text
+'fun'         Keyword
+' '           Text
+'R'           Name
+' '           Text
+"R'"          Name
+' '           Text
+'=>'          Operator
+' '           Text
+'op'          Name
+' '           Text
+'R'           Name
+' '           Text
+"R'"          Name
+'\n    '      Text
+'|'           Operator
+' '           Text
+'A'           Name
+' '           Text
+'::'          Operator
+' '           Text
+'tl'          Name
+' '           Text
+'=>'          Operator
+' '           Text
+'fun'         Keyword
+' '           Text
+'R'           Name
+' '           Text
+"R'"          Name
+' '           Text
+'=>'          Operator
+'\n      '    Text
+'forall'      Keyword
+' '           Text
+'x'           Name
+','           Operator
+' '           Text
+'pointwise_lifting' Name
+' '           Text
+'op'          Name
+' '           Text
+'tl'          Name
+' '           Text
+'('           Operator
+'R'           Name
+' '           Text
+'x'           Name
+')'           Operator
+' '           Text
+'('           Operator
+"R'"          Name
+' '           Text
+'x'           Name
+')'           Operator
+'\n  '        Text
+'end'         Keyword
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' The n-ary equivalence relation, defined by lifting the 0-ary [iff] relation. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Definition'  Keyword.Namespace
+' '           Text
+'predicate_equivalence' Name
+' '           Text
+'{'           Operator
+'l'           Name
+' '           Text
+':'           Operator
+' '           Text
+'list'        Name
+' '           Text
+'Type'        Keyword.Type
+'}'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'binary_relation' Name
+' '           Text
+'('           Operator
+'predicate'   Name
+' '           Text
+'l'           Name
+')'           Operator
+' '           Text
+':='          Operator
+'\n  '        Text
+'pointwise_lifting' Name
+' '           Text
+'iff'         Name
+' '           Text
+'l'           Name
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' The n-ary implication relation, defined by lifting the 0-ary [impl] relation. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Definition'  Keyword.Namespace
+' '           Text
+'predicate_implication' Name
+' '           Text
+'{'           Operator
+'l'           Name
+' '           Text
+':'           Operator
+' '           Text
+'list'        Name
+' '           Text
+'Type'        Keyword.Type
+'}'           Operator
+' '           Text
+':='          Operator
+'\n  '        Text
+'pointwise_lifting' Name
+' '           Text
+'impl'        Name
+' '           Text
+'l'           Name
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' Notations for pointwise equivalence and implication of predicates. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Infix'       Name
+' '           Text
+'"'           Literal.String.Double
+'<∙>'         Literal.String.Double
+'"'           Literal.String.Double
+' '           Text
+':='          Operator
+' '           Text
+'predicate_equivalence' Name
+' '           Text
+'('           Operator
+'at'          Name
+' '           Text
+'level'       Name
+' '           Text
+'95'          Literal.Number.Integer
+','           Operator
+' '           Text
+'no'          Name
+' '           Text
+'associativity' Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'predicate_scope' Name
+'.'           Operator
+'\n'          Text
+
+'Infix'       Name
+' '           Text
+'"'           Literal.String.Double
+'-∙>'         Literal.String.Double
+'"'           Literal.String.Double
+' '           Text
+':='          Operator
+' '           Text
+'predicate_implication' Name
+' '           Text
+'('           Operator
+'at'          Name
+' '           Text
+'level'       Name
+' '           Text
+'70'          Literal.Number.Integer
+','           Operator
+' '           Text
+'right'       Keyword
+' '           Text
+'associativity' Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'predicate_scope' Name
+'.'           Operator
+'\n\n'        Text
+
+'Open'        Keyword.Namespace
+' '           Text
+'Local'       Keyword.Namespace
+' '           Text
+'Scope'       Keyword.Namespace
+' '           Text
+'predicate_scope' Name
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' The pointwise liftings of conjunction and disjunctions.\n   Note that these are [binary_operation]s, building new relations out of old ones. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Definition'  Keyword.Namespace
+' '           Text
+'predicate_intersection' Name
+' '           Text
+':='          Operator
+' '           Text
+'pointwise_extension' Name
+' '           Text
+'and'         Name
+'.'           Operator
+'\n'          Text
+
+'Definition'  Keyword.Namespace
+' '           Text
+'predicate_union' Name
+' '           Text
+':='          Operator
+' '           Text
+'pointwise_extension' Name
+' '           Text
+'or'          Name
+'.'           Operator
+'\n\n'        Text
+
+'Infix'       Name
+' '           Text
+'"'           Literal.String.Double
+'/∙\\'        Literal.String.Double
+'"'           Literal.String.Double
+' '           Text
+':='          Operator
+' '           Text
+'predicate_intersection' Name
+' '           Text
+'('           Operator
+'at'          Name
+' '           Text
+'level'       Name
+' '           Text
+'80'          Literal.Number.Integer
+','           Operator
+' '           Text
+'right'       Keyword
+' '           Text
+'associativity' Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'predicate_scope' Name
+'.'           Operator
+'\n'          Text
+
+'Infix'       Name
+' '           Text
+'"'           Literal.String.Double
+'\\∙/'        Literal.String.Double
+'"'           Literal.String.Double
+' '           Text
+':='          Operator
+' '           Text
+'predicate_union' Name
+' '           Text
+'('           Operator
+'at'          Name
+' '           Text
+'level'       Name
+' '           Text
+'85'          Literal.Number.Integer
+','           Operator
+' '           Text
+'right'       Keyword
+' '           Text
+'associativity' Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'predicate_scope' Name
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' The always [True] and always [False] predicates. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Fixpoint'    Keyword.Namespace
+' '           Text
+'true'        Name.Builtin.Pseudo
+'_'           Operator
+'predicate'   Name
+' '           Text
+'{'           Operator
+'l'           Name
+' '           Text
+':'           Operator
+' '           Text
+'list'        Name
+' '           Text
+'Type'        Keyword.Type
+'}'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'predicate'   Name
+' '           Text
+'l'           Name
+' '           Text
+':='          Operator
+'\n  '        Text
+'match'       Keyword
+' '           Text
+'l'           Name
+' '           Text
+'with'        Keyword
+'\n    '      Text
+'|'           Operator
+' '           Text
+'nil'         Name
+' '           Text
+'=>'          Operator
+' '           Text
+'True'        Name
+'\n    '      Text
+'|'           Operator
+' '           Text
+'A'           Name
+' '           Text
+'::'          Operator
+' '           Text
+'tl'          Name
+' '           Text
+'=>'          Operator
+' '           Text
+'fun'         Keyword
+' '           Text
+'_'           Operator
+' '           Text
+'=>'          Operator
+' '           Text
+'@'           Operator
+'true'        Name.Builtin.Pseudo
+'_'           Operator
+'predicate'   Name
+' '           Text
+'tl'          Name
+'\n  '        Text
+'end'         Keyword
+'.'           Operator
+'\n\n'        Text
+
+'Fixpoint'    Keyword.Namespace
+' '           Text
+'false'       Name.Builtin.Pseudo
+'_'           Operator
+'predicate'   Name
+' '           Text
+'{'           Operator
+'l'           Name
+' '           Text
+':'           Operator
+' '           Text
+'list'        Name
+' '           Text
+'Type'        Keyword.Type
+'}'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'predicate'   Name
+' '           Text
+'l'           Name
+' '           Text
+':='          Operator
+'\n  '        Text
+'match'       Keyword
+' '           Text
+'l'           Name
+' '           Text
+'with'        Keyword
+'\n    '      Text
+'|'           Operator
+' '           Text
+'nil'         Name
+' '           Text
+'=>'          Operator
+' '           Text
+'False'       Name
+'\n    '      Text
+'|'           Operator
+' '           Text
+'A'           Name
+' '           Text
+'::'          Operator
+' '           Text
+'tl'          Name
+' '           Text
+'=>'          Operator
+' '           Text
+'fun'         Keyword
+' '           Text
+'_'           Operator
+' '           Text
+'=>'          Operator
+' '           Text
+'@'           Operator
+'false'       Name.Builtin.Pseudo
+'_'           Operator
+'predicate'   Name
+' '           Text
+'tl'          Name
+'\n  '        Text
+'end'         Keyword
+'.'           Operator
+'\n\n'        Text
+
+'Notation'    Keyword.Namespace
+' '           Text
+'"'           Literal.String.Double
+'∙⊤∙'         Literal.String.Double
+'"'           Literal.String.Double
+' '           Text
+':='          Operator
+' '           Text
+'true'        Name.Builtin.Pseudo
+'_'           Operator
+'predicate'   Name
+' '           Text
+':'           Operator
+' '           Text
+'predicate_scope' Name
+'.'           Operator
+'\n'          Text
+
+'Notation'    Keyword.Namespace
+' '           Text
+'"'           Literal.String.Double
+'∙⊥∙'         Literal.String.Double
+'"'           Literal.String.Double
+' '           Text
+':='          Operator
+' '           Text
+'false'       Name.Builtin.Pseudo
+'_'           Operator
+'predicate'   Name
+' '           Text
+':'           Operator
+' '           Text
+'predicate_scope' Name
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' Predicate equivalence is an equivalence, and predicate implication defines a preorder. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Program'     Name
+' '           Text
+'Instance'    Keyword.Namespace
+' '           Text
+'predicate_equivalence_equivalence' Name
+' '           Text
+':'           Operator
+' '           Text
+'Equivalence' Name
+' '           Text
+'('           Operator
+'@'           Operator
+'predicate_equivalence' Name
+' '           Text
+'l'           Name
+')'           Operator
+'.'           Operator
+'\n  '        Text
+'Next'        Name
+' '           Text
+'Obligation'  Name
+'.'           Operator
+'\n    '      Text
+'induction'   Keyword
+' '           Text
+'l'           Name
+' '           Text
+';'           Operator
+' '           Text
+'firstorder'  Name
+'.'           Operator
+'\n  '        Text
+'Qed'         Keyword.Namespace
+'.'           Operator
+'\n  '        Text
+'Next'        Name
+' '           Text
+'Obligation'  Name
+'.'           Operator
+'\n    '      Text
+'induction'   Keyword
+' '           Text
+'l'           Name
+' '           Text
+';'           Operator
+' '           Text
+'firstorder'  Name
+'.'           Operator
+'\n  '        Text
+'Qed'         Keyword.Namespace
+'.'           Operator
+'\n  '        Text
+'Next'        Name
+' '           Text
+'Obligation'  Name
+'.'           Operator
+'\n    '      Text
+'fold'        Keyword
+' '           Text
+'pointwise_lifting' Name
+'.'           Operator
+'\n    '      Text
+'induction'   Keyword
+' '           Text
+'l'           Name
+'.'           Operator
+' '           Text
+'firstorder'  Name
+'.'           Operator
+'\n    '      Text
+'intros'      Keyword
+'.'           Operator
+' '           Text
+'simpl'       Keyword
+' '           Text
+'in'          Keyword
+' '           Text
+'*'           Operator
+'.'           Operator
+' '           Text
+'pose'        Keyword
+' '           Text
+'('           Operator
+'IHl'         Name
+' '           Text
+'('           Operator
+'x'           Name
+' '           Text
+'x0'          Name
+')'           Operator
+' '           Text
+'('           Operator
+'y'           Name
+' '           Text
+'x0'          Name
+')'           Operator
+' '           Text
+'('           Operator
+'z'           Name
+' '           Text
+'x0'          Name
+')'           Operator
+')'           Operator
+'.'           Operator
+'\n    '      Text
+'firstorder'  Name
+'.'           Operator
+'\n  '        Text
+'Qed'         Keyword.Namespace
+'.'           Operator
+'\n\n'        Text
+
+'Program'     Name
+' '           Text
+'Instance'    Keyword.Namespace
+' '           Text
+'predicate_implication_preorder' Name
+' '           Text
+':'           Operator
+'\n  '        Text
+'PreOrder'    Name
+' '           Text
+'('           Operator
+'@'           Operator
+'predicate_implication' Name
+' '           Text
+'l'           Name
+')'           Operator
+'.'           Operator
+'\n  '        Text
+'Next'        Name
+' '           Text
+'Obligation'  Name
+'.'           Operator
+'\n    '      Text
+'induction'   Keyword
+' '           Text
+'l'           Name
+' '           Text
+';'           Operator
+' '           Text
+'firstorder'  Name
+'.'           Operator
+'\n  '        Text
+'Qed'         Keyword.Namespace
+'.'           Operator
+'\n  '        Text
+'Next'        Name
+' '           Text
+'Obligation'  Name
+'.'           Operator
+'\n    '      Text
+'induction'   Keyword
+' '           Text
+'l'           Name
+'.'           Operator
+' '           Text
+'firstorder'  Name
+'.'           Operator
+'\n    '      Text
+'unfold'      Keyword
+' '           Text
+'predicate_implication' Name
+' '           Text
+'in'          Keyword
+' '           Text
+'*'           Operator
+'.'           Operator
+' '           Text
+'simpl'       Keyword
+' '           Text
+'in'          Keyword
+' '           Text
+'*'           Operator
+'.'           Operator
+'\n    '      Text
+'intro'       Keyword
+'.'           Operator
+' '           Text
+'pose'        Keyword
+' '           Text
+'('           Operator
+'IHl'         Name
+' '           Text
+'('           Operator
+'x'           Name
+' '           Text
+'x0'          Name
+')'           Operator
+' '           Text
+'('           Operator
+'y'           Name
+' '           Text
+'x0'          Name
+')'           Operator
+' '           Text
+'('           Operator
+'z'           Name
+' '           Text
+'x0'          Name
+')'           Operator
+')'           Operator
+'.'           Operator
+' '           Text
+'firstorder'  Name
+'.'           Operator
+'\n  '        Text
+'Qed'         Keyword.Namespace
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' We define the various operations which define the algebra on binary relations,\n   from the general ones. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Definition'  Keyword.Namespace
+' '           Text
+'relation_equivalence' Name
+' '           Text
+'{'           Operator
+'A'           Name
+' '           Text
+':'           Operator
+' '           Text
+'Type'        Keyword.Type
+'}'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'('           Operator
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+':='          Operator
+'\n  '        Text
+'@'           Operator
+'predicate_equivalence' Name
+' '           Text
+'('           Operator
+'_'           Operator
+'::'          Operator
+'_'           Operator
+'::'          Operator
+'nil'         Name
+')'           Operator
+'.'           Operator
+'\n\n'        Text
+
+'Class'       Keyword.Namespace
+' '           Text
+'subrelation' Name
+' '           Text
+'{'           Operator
+'A'           Name
+':'           Operator
+'Type'        Keyword.Type
+'}'           Operator
+' '           Text
+'('           Operator
+'R'           Name
+' '           Text
+"R'"          Name
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'Prop'        Keyword.Type
+' '           Text
+':='          Operator
+'\n  '        Text
+'is_subrelation' Name
+' '           Text
+':'           Operator
+' '           Text
+'@'           Operator
+'predicate_implication' Name
+' '           Text
+'('           Operator
+'A'           Name
+'::'          Operator
+'A'           Name
+'::'          Operator
+'nil'         Name
+')'           Operator
+' '           Text
+'R'           Name
+' '           Text
+"R'"          Name
+'.'           Operator
+'\n\n'        Text
+
+'Implicit'    Keyword.Namespace
+' '           Text
+'Arguments'   Keyword.Namespace
+' '           Text
+'subrelation' Name
+' '           Text
+'['           Operator
+'['           Operator
+'A'           Name
+']'           Operator
+']'           Operator
+'.'           Operator
+'\n\n'        Text
+
+'Definition'  Keyword.Namespace
+' '           Text
+'relation_conjunction' Name
+' '           Text
+'{'           Operator
+'A'           Name
+'}'           Operator
+' '           Text
+'('           Operator
+'R'           Name
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+'('           Operator
+"R'"          Name
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+' '           Text
+':='          Operator
+'\n  '        Text
+'@'           Operator
+'predicate_intersection' Name
+' '           Text
+'('           Operator
+'A'           Name
+'::'          Operator
+'A'           Name
+'::'          Operator
+'nil'         Name
+')'           Operator
+' '           Text
+'R'           Name
+' '           Text
+"R'"          Name
+'.'           Operator
+'\n\n'        Text
+
+'Definition'  Keyword.Namespace
+' '           Text
+'relation_disjunction' Name
+' '           Text
+'{'           Operator
+'A'           Name
+'}'           Operator
+' '           Text
+'('           Operator
+'R'           Name
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+'('           Operator
+"R'"          Name
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+' '           Text
+':='          Operator
+'\n  '        Text
+'@'           Operator
+'predicate_union' Name
+' '           Text
+'('           Operator
+'A'           Name
+'::'          Operator
+'A'           Name
+'::'          Operator
+'nil'         Name
+')'           Operator
+' '           Text
+'R'           Name
+' '           Text
+"R'"          Name
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' Relation equivalence is an equivalence, and subrelation defines a partial order. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Set'         Keyword.Namespace
+' '           Text
+'Automatic'   Name
+' '           Text
+'Introduction' Name
+'.'           Operator
+'\n\n'        Text
+
+'Instance'    Keyword.Namespace
+' '           Text
+'relation_equivalence_equivalence' Name
+' '           Text
+'('           Operator
+'A'           Name
+' '           Text
+':'           Operator
+' '           Text
+'Type'        Keyword.Type
+')'           Operator
+' '           Text
+':'           Operator
+'\n  '        Text
+'Equivalence' Name
+' '           Text
+'('           Operator
+'@'           Operator
+'relation_equivalence' Name
+' '           Text
+'A'           Name
+')'           Operator
+'.'           Operator
+'\n'          Text
+
+'Proof'       Keyword.Namespace
+'.'           Operator
+' '           Text
+'exact'       Keyword.Pseudo
+' '           Text
+'('           Operator
+'@'           Operator
+'predicate_equivalence_equivalence' Name
+' '           Text
+'('           Operator
+'A'           Name
+'::'          Operator
+'A'           Name
+'::'          Operator
+'nil'         Name
+')'           Operator
+')'           Operator
+'.'           Operator
+' '           Text
+'Qed'         Keyword.Namespace
+'.'           Operator
+'\n\n'        Text
+
+'Instance'    Keyword.Namespace
+' '           Text
+'relation_implication_preorder' Name
+' '           Text
+'A'           Name
+' '           Text
+':'           Operator
+' '           Text
+'PreOrder'    Name
+' '           Text
+'('           Operator
+'@'           Operator
+'subrelation' Name
+' '           Text
+'A'           Name
+')'           Operator
+'.'           Operator
+'\n'          Text
+
+'Proof'       Keyword.Namespace
+'.'           Operator
+' '           Text
+'exact'       Keyword.Pseudo
+' '           Text
+'('           Operator
+'@'           Operator
+'predicate_implication_preorder' Name
+' '           Text
+'('           Operator
+'A'           Name
+'::'          Operator
+'A'           Name
+'::'          Operator
+'nil'         Name
+')'           Operator
+')'           Operator
+'.'           Operator
+' '           Text
+'Qed'         Keyword.Namespace
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' '           Comment
+'*'           Comment
+'*'           Comment
+'*'           Comment
+' Partial Order.\n   A partial order is a preorder which is additionally antisymmetric.\n   We give an equivalent definition, up-to an equivalence relation\n   on the carrier. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Class'       Keyword.Namespace
+' '           Text
+'PartialOrder' Name
+' '           Text
+'{'           Operator
+'A'           Name
+'}'           Operator
+' '           Text
+'eqA'         Name
+' '           Text
+'`'           Operator
+'{'           Operator
+'equ'         Name
+' '           Text
+':'           Operator
+' '           Text
+'Equivalence' Name
+' '           Text
+'A'           Name
+' '           Text
+'eqA'         Name
+'}'           Operator
+' '           Text
+'R'           Name
+' '           Text
+'`'           Operator
+'{'           Operator
+'preo'        Name
+' '           Text
+':'           Operator
+' '           Text
+'PreOrder'    Name
+' '           Text
+'A'           Name
+' '           Text
+'R'           Name
+'}'           Operator
+' '           Text
+':='          Operator
+'\n  '        Text
+'partial_order_equivalence' Name
+' '           Text
+':'           Operator
+' '           Text
+'relation_equivalence' Name
+' '           Text
+'eqA'         Name
+' '           Text
+'('           Operator
+'relation_conjunction' Name
+' '           Text
+'R'           Name
+' '           Text
+'('           Operator
+'inverse'     Name
+' '           Text
+'R'           Name
+')'           Operator
+')'           Operator
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' The equivalence proof is sufficient for proving that [R] must be a morphism\n   for equivalence ' Comment
+'('           Comment
+'see Morphisms' Comment
+')'           Comment
+'.\n   It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Instance'    Keyword.Namespace
+' '           Text
+'partial_order_antisym' Name
+' '           Text
+'`'           Operator
+'('           Operator
+'PartialOrder' Name
+' '           Text
+'A'           Name
+' '           Text
+'eqA'         Name
+' '           Text
+'R'           Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'!'           Operator
+' '           Text
+'Antisymmetric' Name
+' '           Text
+'A'           Name
+' '           Text
+'eqA'         Name
+' '           Text
+'R'           Name
+'.'           Operator
+'\n'          Text
+
+'Proof'       Keyword.Namespace
+' '           Text
+'with'        Keyword
+' '           Text
+'auto'        Keyword
+'.'           Operator
+'\n  '        Text
+'reduce_goal' Name
+'.'           Operator
+'\n  '        Text
+'pose'        Keyword
+' '           Text
+'proof'       Name
+' '           Text
+'partial_order_equivalence' Name
+' '           Text
+'as'          Keyword
+' '           Text
+'poe'         Name
+'.'           Operator
+' '           Text
+'do'          Keyword.Reserved
+' '           Text
+'3'           Literal.Number.Integer
+' '           Text
+'red'         Keyword
+' '           Text
+'in'          Keyword
+' '           Text
+'poe'         Name
+'.'           Operator
+'\n  '        Text
+'apply'       Keyword
+' '           Text
+'<-'          Operator
+' '           Text
+'poe'         Name
+'.'           Operator
+' '           Text
+'firstorder'  Name
+'.'           Operator
+'\n'          Text
+
+'Qed'         Keyword.Namespace
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' The partial order defined by subrelation and relation equivalence. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Program'     Name
+' '           Text
+'Instance'    Keyword.Namespace
+' '           Text
+'subrelation_partial_order' Name
+' '           Text
+':'           Operator
+'\n  '        Text
+'!'           Operator
+' '           Text
+'PartialOrder' Name
+' '           Text
+'('           Operator
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+'relation_equivalence' Name
+' '           Text
+'subrelation' Name
+'.'           Operator
+'\n\n  '      Text
+'Next'        Name
+' '           Text
+'Obligation'  Name
+'.'           Operator
+'\n  '        Text
+'Proof'       Keyword.Namespace
+'.'           Operator
+'\n    '      Text
+'unfold'      Keyword
+' '           Text
+'relation_equivalence' Name
+' '           Text
+'in'          Keyword
+' '           Text
+'*'           Operator
+'.'           Operator
+' '           Text
+'firstorder'  Name
+'.'           Operator
+'\n  '        Text
+'Qed'         Keyword.Namespace
+'.'           Operator
+'\n\n'        Text
+
+'Typeclasses' Name
+' '           Text
+'Opaque'      Name
+' '           Text
+'arrows'      Name
+' '           Text
+'predicate_implication' Name
+' '           Text
+'predicate_equivalence' Name
+'\n  '        Text
+'relation_equivalence' Name
+' '           Text
+'pointwise_lifting' Name
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' Rewrite relation on a given support: declares a relation as a rewrite\n   relation for use by the generalized rewriting tactic.\n   It helps choosing if a rewrite should be handled\n   by the generalized or the regular rewriting tactic using leibniz equality.\n   Users can declare an [RewriteRelation A RA] anywhere to declare default\n   relations. This is also done automatically by the [Declare Relation A RA]\n   commands. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Class'       Keyword.Namespace
+' '           Text
+'RewriteRelation' Name
+' '           Text
+'{'           Operator
+'A'           Name
+' '           Text
+':'           Operator
+' '           Text
+'Type'        Keyword.Type
+'}'           Operator
+' '           Text
+'('           Operator
+'RA'          Name
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+'.'           Operator
+'\n\n'        Text
+
+'Instance'    Keyword.Namespace
+':'           Operator
+' '           Text
+'RewriteRelation' Name
+' '           Text
+'impl'        Name
+'.'           Operator
+'\n'          Text
+
+'Instance'    Keyword.Namespace
+':'           Operator
+' '           Text
+'RewriteRelation' Name
+' '           Text
+'iff'         Name
+'.'           Operator
+'\n'          Text
+
+'Instance'    Keyword.Namespace
+':'           Operator
+' '           Text
+'RewriteRelation' Name
+' '           Text
+'('           Operator
+'@'           Operator
+'relation_equivalence' Name
+' '           Text
+'A'           Name
+')'           Operator
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' Any [Equivalence] declared in the context is automatically considered\n   a rewrite relation. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Instance'    Keyword.Namespace
+' '           Text
+'equivalence_rewrite_relation' Name
+' '           Text
+'`'           Operator
+'('           Operator
+'Equivalence' Name
+' '           Text
+'A'           Name
+' '           Text
+'eqA'         Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'RewriteRelation' Name
+' '           Text
+'eqA'         Name
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' Strict Order ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Class'       Keyword.Namespace
+' '           Text
+'StrictOrder' Name
+' '           Text
+'{'           Operator
+'A'           Name
+' '           Text
+':'           Operator
+' '           Text
+'Type'        Keyword.Type
+'}'           Operator
+' '           Text
+'('           Operator
+'R'           Name
+' '           Text
+':'           Operator
+' '           Text
+'relation'    Name
+' '           Text
+'A'           Name
+')'           Operator
+' '           Text
+':='          Operator
+' '           Text
+'{'           Operator
+'\n  '        Text
+'StrictOrder_Irreflexive' Name
+' '           Text
+':>'          Operator
+' '           Text
+'Irreflexive' Name
+' '           Text
+'R'           Name
+' '           Text
+';'           Operator
+'\n  '        Text
+'StrictOrder_Transitive' Name
+' '           Text
+':>'          Operator
+' '           Text
+'Transitive'  Name
+' '           Text
+'R'           Name
+'\n'          Text
+
+'}'           Operator
+'.'           Operator
+'\n\n'        Text
+
+'Instance'    Keyword.Namespace
+' '           Text
+'StrictOrder_Asymmetric' Name
+' '           Text
+'`'           Operator
+'('           Operator
+'StrictOrder' Name
+' '           Text
+'A'           Name
+' '           Text
+'R'           Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'Asymmetric'  Name
+' '           Text
+'R'           Name
+'.'           Operator
+'\n'          Text
+
+'Proof'       Keyword.Namespace
+'.'           Operator
+' '           Text
+'firstorder'  Name
+'.'           Operator
+' '           Text
+'Qed'         Keyword.Namespace
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' Inversing a [StrictOrder] gives another [StrictOrder] ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Lemma'       Keyword.Namespace
+' '           Text
+'StrictOrder_inverse' Name
+' '           Text
+'`'           Operator
+'('           Operator
+'StrictOrder' Name
+' '           Text
+'A'           Name
+' '           Text
+'R'           Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'StrictOrder' Name
+' '           Text
+'('           Operator
+'inverse'     Name
+' '           Text
+'R'           Name
+')'           Operator
+'.'           Operator
+'\n'          Text
+
+'Proof'       Keyword.Namespace
+'.'           Operator
+' '           Text
+'firstorder'  Name
+'.'           Operator
+' '           Text
+'Qed'         Keyword.Namespace
+'.'           Operator
+'\n\n'        Text
+
+'(*'          Comment
+'*'           Comment
+' Same for [PartialOrder]. ' Comment
+'*)'          Comment
+'\n\n'        Text
+
+'Lemma'       Keyword.Namespace
+' '           Text
+'PreOrder_inverse' Name
+' '           Text
+'`'           Operator
+'('           Operator
+'PreOrder'    Name
+' '           Text
+'A'           Name
+' '           Text
+'R'           Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'PreOrder'    Name
+' '           Text
+'('           Operator
+'inverse'     Name
+' '           Text
+'R'           Name
+')'           Operator
+'.'           Operator
+'\n'          Text
+
+'Proof'       Keyword.Namespace
+'.'           Operator
+' '           Text
+'firstorder'  Name
+'.'           Operator
+' '           Text
+'Qed'         Keyword.Namespace
+'.'           Operator
+'\n\n'        Text
+
+'Hint'        Keyword.Namespace
+' '           Text
+'Extern'      Name
+' '           Text
+'3'           Literal.Number.Integer
+' '           Text
+'('           Operator
+'StrictOrder' Name
+' '           Text
+'('           Operator
+'inverse'     Name
+' '           Text
+'_'           Operator
+')'           Operator
+')'           Operator
+' '           Text
+'=>'          Operator
+' '           Text
+'class_apply' Name
+' '           Text
+'StrictOrder_inverse' Name
+' '           Text
+':'           Operator
+' '           Text
+'typeclass_instances' Name
+'.'           Operator
+'\n'          Text
+
+'Hint'        Keyword.Namespace
+' '           Text
+'Extern'      Name
+' '           Text
+'3'           Literal.Number.Integer
+' '           Text
+'('           Operator
+'PreOrder'    Name
+' '           Text
+'('           Operator
+'inverse'     Name
+' '           Text
+'_'           Operator
+')'           Operator
+')'           Operator
+' '           Text
+'=>'          Operator
+' '           Text
+'class_apply' Name
+' '           Text
+'PreOrder_inverse' Name
+' '           Text
+':'           Operator
+' '           Text
+'typeclass_instances' Name
+'.'           Operator
+'\n\n'        Text
+
+'Lemma'       Keyword.Namespace
+' '           Text
+'PartialOrder_inverse' Name
+' '           Text
+'`'           Operator
+'('           Operator
+'PartialOrder' Name
+' '           Text
+'A'           Name
+' '           Text
+'eqA'         Name
+' '           Text
+'R'           Name
+')'           Operator
+' '           Text
+':'           Operator
+' '           Text
+'PartialOrder' Name
+' '           Text
+'eqA'         Name
+' '           Text
+'('           Operator
+'inverse'     Name
+' '           Text
+'R'           Name
+')'           Operator
+'.'           Operator
+'\n'          Text
+
+'Proof'       Keyword.Namespace
+'.'           Operator
+' '           Text
+'firstorder'  Name
+'.'           Operator
+' '           Text
+'Qed'         Keyword.Namespace
+'.'           Operator
+'\n\n'        Text
+
+'Hint'        Keyword.Namespace
+' '           Text
+'Extern'      Name
+' '           Text
+'3'           Literal.Number.Integer
+' '           Text
+'('           Operator
+'PartialOrder' Name
+' '           Text
+'('           Operator
+'inverse'     Name
+' '           Text
+'_'           Operator
+')'           Operator
+')'           Operator
+' '           Text
+'=>'          Operator
+' '           Text
+'class_apply' Name
+' '           Text
+'PartialOrder_inverse' Name
+' '           Text
+':'           Operator
+' '           Text
+'typeclass_instances' Name
+'.'           Operator
+'\n'          Text