diff --git a/.gitmodules b/.gitmodules
index f2c90a1cad..1bbf1fd2bd 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1193,6 +1193,9 @@
 [submodule "vendor/grammars/sublime-golo"]
 	path = vendor/grammars/sublime-golo
 	url = https://github.com/TypeUnsafe/sublime-golo
+[submodule "vendor/grammars/sublime-lambdapi"]
+	path = vendor/grammars/sublime-lambdapi
+	url = https://github.com/Deducteam/sublime-lambdapi.git
 [submodule "vendor/grammars/sublime-mask"]
 	path = vendor/grammars/sublime-mask
 	url = https://github.com/tenbits/sublime-mask
diff --git a/grammars.yml b/grammars.yml
index 9da8a9b6a2..53d5b8ce9c 100644
--- a/grammars.yml
+++ b/grammars.yml
@@ -1073,6 +1073,8 @@ vendor/grammars/sublime-glsl:
 - source.glsl
 vendor/grammars/sublime-golo:
 - source.golo
+vendor/grammars/sublime-lambdapi:
+- source.lp
 vendor/grammars/sublime-mask:
 - source.mask
 vendor/grammars/sublime-nearley:
diff --git a/lib/linguist/heuristics.yml b/lib/linguist/heuristics.yml
index ddaacd9e6b..2555e2ccae 100644
--- a/lib/linguist/heuristics.yml
+++ b/lib/linguist/heuristics.yml
@@ -443,6 +443,8 @@ disambiguations:
     pattern: '^import [A-Z]'
 - extensions: ['.lp']
   rules:
+  - language: Lambdapi
+    pattern: '(?:^|\s)symbol(?:$|\s)|(?:^|\s)rule(?:$|\s)'
   - language: Linear Programming
     pattern: '^(?i:minimize|minimum|min|maximize|maximum|max)(?i:\s+multi-objectives)?$'
   - language: Answer Set Programming
diff --git a/lib/linguist/languages.yml b/lib/linguist/languages.yml
index 971b8138eb..fa7ab7ba5b 100644
--- a/lib/linguist/languages.yml
+++ b/lib/linguist/languages.yml
@@ -4011,6 +4011,14 @@ LabVIEW:
   codemirror_mode: xml
   codemirror_mime_type: text/xml
   language_id: 194
+Lambdapi:
+  type: programming
+  color: "#8027a3"
+  extensions:
+  - ".lp"
+  tm_scope: source.lp
+  ace_mode: text
+  language_id: 759240513
 Lark:
   type: data
   color: "#2980B9"
diff --git a/samples/Lambdapi/List.lp b/samples/Lambdapi/List.lp
new file mode 100644
index 0000000000..e4acd2be82
--- /dev/null
+++ b/samples/Lambdapi/List.lp
@@ -0,0 +1,342 @@
+require open tests.OK.Set tests.OK.Prop tests.OK.FOL tests.OK.Eq
+  tests.OK.Nat tests.OK.Bool;
+
+(a:Set) inductive 𝕃:TYPE ≔
+| □ : 𝕃 a // \Box
+| ⸬ : τ a → 𝕃 a → 𝕃 a; // ::
+
+notation ⸬ infix right 20;
+
+// set code for 𝕃
+
+constant symbol list : Set → Set;
+
+rule τ (list $a) ↪ 𝕃 $a;
+
+// is□
+
+symbol is□ [a]: 𝕃 a → 𝔹;
+
+rule is□ □ ↪ true
+with is□ (_ ⸬ _) ↪ false;
+
+// non confusion of constructors
+
+opaque symbol ⸬≠□ [a] [x:τ a] [l] : π (x ⸬ l ≠ □) ≔
+begin
+  assume a x l h; refine ind_eq h (λ l, istrue(is□ l)) ⊤ᵢ
+end;
+
+opaque symbol □≠⸬ [a] [x:τ a] [l] : π (□ ≠ x ⸬ l) ≔
+begin
+  assume a x l h; apply @⸬≠□ a x l; symmetry; apply h
+end;
+
+// head
+
+symbol head [a] : τ a → 𝕃 a → τ a;
+
+rule head $x □ ↪ $x
+with head _ ($x ⸬ _) ↪ $x;
+
+// tail
+
+symbol behead [a] : 𝕃 a → 𝕃 a;
+
+rule behead □ ↪ □
+with behead (_ ⸬ $l) ↪ $l;
+
+// injectivity of constructors
+
+opaque symbol ⸬_inj [a] [x:τ a] [l y m] : π(x ⸬ l = y ⸬ m) → π(x = y ∧ l = m) ≔
+begin
+  assume a x l y m e; apply ∧ᵢ { refine feq (head x) e } { refine feq behead e }
+end;
+
+// boolean equality on lists
+
+symbol eql [a] : (τ a → τ a → 𝔹) → 𝕃 a → 𝕃 a → 𝔹;
+
+rule eql _ □ □ ↪ true
+with eql _ (_ ⸬ _) □ ↪ false
+with eql _ □ (_ ⸬ _) ↪ false
+with eql $beq ($x ⸬ $l) ($y ⸬ $m) ↪ ($beq $x $y) and (eql $beq $l $m);
+
+opaque symbol eql_correct a (beq:τ a → τ a → 𝔹) :
+  π(`∀ x, `∀ y, beq x y ⇒ x = y) → π(`∀ l, `∀ m, eql beq l m ⇒ l = m) ≔
+begin
+  assume a beq beq_correct; induction
+  { induction
+    { reflexivity }
+    { simplify; assume y m i c; refine ⊥ₑ c }
+  }
+  { assume x l h; induction
+    { simplify; assume c; refine ⊥ₑ c; }
+    { simplify; assume y m i c;
+      apply feq2 (⸬) _ _
+      { apply beq_correct; apply @andₑ₁ _ (eql beq l m) c }
+      { apply h; refine @andₑ₂ (beq x y) _ c
+      } 
+    }
+  }
+end;
+
+opaque symbol eql_complete a (beq : τ a → τ a → 𝔹) :
+  π(`∀ x, `∀ y, x = y ⇒ beq x y) → π(`∀ l, `∀ m, l = m ⇒ eql beq l m) ≔
+begin
+  assume a beq beq_complete; induction
+  { assume m i; rewrite left i; apply ⊤ᵢ; }
+  { assume x l h; induction
+    { assume j; apply ⸬≠□ j; }
+    { assume y m i j; simplify;
+      have j': π(x = y ∧ l = m) { apply ⸬_inj j };
+      apply @istrue_and (beq x y) (eql beq l m); apply ∧ᵢ
+      { apply beq_complete x y; apply ∧ₑ₁ j' }
+      { apply h m; apply ∧ₑ₂ j' }
+    }
+  }
+end;
+
+// size
+
+symbol size [a] : 𝕃 a → ℕ;
+
+rule size □ ↪ 0
+with size (_ ⸬ $l) ↪ size $l +1;
+
+opaque symbol size0nil [a] (l:𝕃 a) : π (size l = 0) → π (l = □) ≔
+begin
+  assume a; induction
+  { reflexivity; }
+  { assume e l h i; apply ⊥ₑ; apply s≠0 i; }
+end;
+
+symbol nilp [a] l ≔ is0 (@size a l);
+
+opaque symbol size_behead [a] (l:𝕃 a) : π (size (behead l) = size l ∸1) ≔
+begin
+  assume a; induction
+  { reflexivity; }
+  { assume e l h; reflexivity; }
+end;
+
+// concatenation
+
+symbol ++ [a] : 𝕃 a → 𝕃 a → 𝕃 a; notation ++ infix right 30; // \cdot
+
+assert x y z ⊢ x ++ y ++ z ≡ x ++ (y ++ z);
+assert x l m ⊢ x ⸬ l ++ m ≡ x ⸬ (l ++ m);
+
+rule □ ++ $m ↪ $m
+with ($x ⸬ $l) ++ $m ↪ $x ⸬ ($l ++ $m);
+
+opaque symbol cat0s [a] (l:𝕃 a) : π (□ ++ l = l) ≔
+begin
+  reflexivity;
+end;
+
+opaque symbol cat1s [a] (x:τ a) l : π ((x ⸬ □) ++ l = (x ⸬ l)) ≔
+begin
+  reflexivity;
+end;
+
+opaque symbol cat_cons [a] (x:τ a) l1 l2 : π ((x ⸬ l1) ++ l2 = x ⸬ (l1 ++ l2)) ≔
+begin
+  reflexivity;
+end;
+
+// nseq
+
+symbol nseq [a] : ℕ → τ a → 𝕃 a;
+
+rule nseq 0 _ ↪ □
+with nseq ($n +1) $x ↪ $x ⸬ (nseq $n $x);
+
+// ncons
+
+symbol ncons [a] : ℕ → τ a → 𝕃 a → 𝕃 a;
+
+rule ncons 0 _ $l ↪ $l
+with ncons ($n +1) $x $l ↪ $x ⸬ ncons $n $x $l;
+
+opaque symbol size_ncons [a] n (x:τ a) l : π (size (ncons n x l) = n + size l) ≔
+begin
+  assume a; induction
+  { reflexivity; }
+  { assume n h x l; simplify; apply feq (+1) (h x l); }
+end;
+
+opaque symbol size_nseq [a] n (x:τ a) : π (size (nseq n x) = n) ≔
+begin
+  assume a; induction
+  { reflexivity; }
+  { assume n h x; simplify; apply feq (+1) (h x); }
+end;
+
+opaque symbol cat_nseq [a] n (x:τ a) l : π (nseq n x ++ l = ncons n x l) ≔
+begin
+  assume a; induction
+  { reflexivity; }
+  { assume n h x l; simplify; rewrite h x l; reflexivity; }
+end;
+
+opaque symbol nseqD [a] n1 n2 (x:τ a) :
+  π (nseq (n1 + n2) x = nseq n1 x ++ nseq n2 x) ≔
+begin
+  assume a; induction
+  { reflexivity; }
+  { assume n1 h n2 x; simplify; rewrite h n2; reflexivity; }
+end;
+
+opaque symbol cats0 [a] (l:𝕃 a) : π(l ++ □ = l) ≔
+begin
+  assume a;
+  induction
+    // case l = □
+    { reflexivity; }
+    // case l = x ⸬ l'
+    { assume x l' h; simplify; rewrite h; reflexivity; }
+end;
+
+rule $m ++ □ ↪ $m;
+
+opaque symbol size_cat [a] (l m : 𝕃 a) : π(size (l ++ m) = size l + size m) ≔
+begin
+  assume a;
+  induction
+    // case l = □
+    { reflexivity; }
+    // case l = x⸬l'
+    { assume x l' h m; simplify; rewrite h; reflexivity; }
+end;
+
+rule size ($l ++ $m) ↪ size $l + size $m;
+
+opaque symbol catA  [a] (l m n : 𝕃 a) : π((l ++ m) ++ n = l ++ (m ++ n)) ≔
+begin
+  assume a;
+  induction
+    // case l = □
+    { reflexivity; }
+    // case l = x⸬l'
+    { assume x l' h m n; simplify; rewrite h; reflexivity; }
+end;
+
+rule ($l ++ $m) ++ $n ↪ $l ++ ($m ++ $n);
+
+opaque symbol cat_nilp [a] (l1 l2 : 𝕃 a) :
+  π (nilp (l1 ++ l2) = (nilp l1 and nilp l2)) ≔
+begin
+  assume a; induction
+  { reflexivity; }
+  { assume e l h l2; simplify; reflexivity; }
+end;
+
+// list reversal
+
+symbol rev [a] : 𝕃 a → 𝕃 a;
+
+rule rev □ ↪ □
+with rev ($x ⸬ $l) ↪ rev $l ++ ($x ⸬ □);
+
+opaque symbol rev_concat [a] (l m : 𝕃 a) : π(rev (l ++ m) = rev m ++ rev l) ≔
+begin
+  assume a;
+  induction
+    // case l = □
+    { simplify; reflexivity; }
+    // case l = ⸬
+    { assume x l h m; simplify; rewrite h; reflexivity; }
+end;
+
+rule rev ($l ++ $m) ↪ rev $m ++ rev $l;
+
+opaque symbol rev_idem [a] (l :𝕃 a) : π(rev (rev l) = l) ≔
+begin
+  assume a; induction
+  { reflexivity }
+  { assume x l h; simplify; rewrite h; reflexivity }
+end;
+
+opaque symbol size_rev [a] (l : 𝕃 a) : π(size (rev l) = size l) ≔
+begin
+  assume a;
+  induction
+    // case l = □
+    { simplify; reflexivity; }
+    // case l = ⸬
+    { assume x l h; simplify; rewrite h; reflexivity; }
+end;
+
+// rcons
+
+symbol rcons [a] : 𝕃 a → τ a → 𝕃 a;
+
+rule rcons □ $x ↪ $x ⸬ □
+with rcons ($e ⸬ $l) $x ↪ $e ⸬ (rcons $l $x);
+
+opaque symbol cats1 [a] (l:𝕃 a) (z:τ a) : π (l ++ (z ⸬ □) = rcons l z) ≔
+begin
+  assume a; induction
+  { reflexivity; }
+  { assume e l h z; simplify; rewrite h z; reflexivity; }
+end;
+
+opaque symbol rcons_cons [a] (x:τ a) (s:𝕃 a) (z:τ a) :
+  π (rcons (x ⸬ s) z = x ⸬ rcons s z) ≔
+begin
+  reflexivity;
+end;
+
+// Arr
+
+symbol Arr : ℕ → Set → Set → TYPE;
+
+rule Arr 0 _ $b ↪ τ $b
+with Arr ($n +1) $a $b ↪ τ $a → Arr $n $a $b;
+
+// seqn
+
+symbol seqn_acc [a] n : 𝕃 a → Arr n a (list a);
+
+rule seqn_acc 0 $l ↪ rev $l
+with seqn_acc ($n +1) $l $x ↪ seqn_acc $n ($x ⸬ $l);
+
+symbol seqn [a] n ≔ @seqn_acc a n □;
+
+assert a (x y : τ a) ⊢ seqn 2 x y ≡ x ⸬ y ⸬ □;
+
+// iota
+
+symbol iota : ℕ → ℕ → 𝕃 nat;
+rule iota _ 0 ↪ □
+with iota $n ($k +1) ↪ $n ⸬ iota ($n +1) $k;
+
+assert ⊢ iota 1 2 ≡ 1 ⸬ 2 ⸬ □;
+
+// indexes
+
+symbol indexes [a] : 𝕃 a → 𝕃 nat;
+
+rule indexes $l ↪ iota 0 (size $l);
+
+assert x ⊢ indexes (x ⸬ x ⸬ x  ⸬ x ⸬ □) ≡ 0 ⸬ 1 ⸬ 2 ⸬ 3 ⸬ □;
+
+// last
+
+symbol last [a] : τ a → 𝕃 a → τ a;
+
+rule last $x □ ↪ $x
+with last _ ($e ⸬ $l) ↪ last $e $l;
+
+assert ⊢ last 4 (3 ⸬ 2 ⸬ 1 ⸬ □) ≡ 1;
+assert ⊢ last 4 □ ≡ 4;
+
+// belast
+
+symbol belast [a] : τ a → 𝕃 a → 𝕃 a;
+
+rule belast _ □ ↪ □
+with belast $x ($e ⸬ $l) ↪ $x ⸬ belast $e $l;
+
+assert ⊢ belast 4 (3 ⸬ 2 ⸬ 1 ⸬ □) ≡ 4 ⸬ 3 ⸬ 2 ⸬ □;
diff --git a/samples/Lambdapi/tutorial.lp b/samples/Lambdapi/tutorial.lp
new file mode 100644
index 0000000000..35e46cba78
--- /dev/null
+++ b/samples/Lambdapi/tutorial.lp
@@ -0,0 +1,349 @@
+// Learn the basics of Lambdapi in 15 minutes (this is a one-line comment).
+
+/* Install support for Lambdapi files in Emacs or VSCode to better
+visualize this file and the generated subgoals in proofs
+(this is a multi-lines comment). */
+
+/* Put this file and
+https://github.com/Deducteam/lambdapi/blob/master/tests/lambdapi.pkg
+in the same directory, and run emacs or vscode from this
+directory. Make sure that lambdapi is in your path (do "eval `opam
+env`" if you installed lambdapi with opam). */
+
+/* In Lambdapi, you can declare type and object symbols. Symbol names
+can contain unicode characters (utf8). */
+
+/* Convention: identifiers starting with an uppercase letter denote
+types, while identifiers starting with a lowercase letter denote objects. */
+
+symbol ℕ : TYPE; // is a type declaration
+
+// Commands are separated by semi-colons.
+
+symbol zero : ℕ; // is an object declaration
+
+symbol succ : ℕ → ℕ; /* means that "succ" takes an argument of type ℕ
+  and returns something of type ℕ. */
+
+// We can make definitions as follows:
+symbol one ≔ succ zero;
+
+// We can ask Lambdapi the type of a term:
+type one;
+
+// We can check that a term has a given type:
+assert ⊢ one : ℕ;
+
+// or that a term does not have a given type:
+assertnot ⊢ succ : ℕ;
+
+symbol + : ℕ → ℕ → ℕ;
+notation + infix right 10;
+/* means that + is declared as infix.
+"right" means that "x + y + z" is the same as "x + (y + z)".
+10 is the priority level of +. It is useful to parse expressions
+with various infix operators (see below). */
+
+symbol × : ℕ → ℕ → ℕ;
+notation × infix right 20;
+/* The priority level of × is higher than the one of +.
+So "x + y × z" is parsed as "x + (y × z)". We can check it as follows: */
+
+assert x y z ⊢ x + y × z ≡ x + (y × z);
+assertnot x y z ⊢ x + y × z ≡ (x + y) × z;
+
+/* We can now tell Lambdapi to identify any term of the form "t + 0" with "t"
+by simply declaring the following rewrite rule: */
+rule $x + zero ↪ $x; // rule variables must be prefixed by "$"
+
+// We can also ask Lambdapi to evaluate a term using the declared rules:
+compute zero + zero;
+// and check the result:
+assert ⊢ zero + zero ≡ zero;
+  /* ≡ is the equational theory generated by the user-defined rules
+     and β-reduction + η-reduction if the flag "eta_equality" is on. */
+
+// The definition of + can be completed by adding a new rule later:
+rule $x + succ $y ↪ succ ($x + $y);
+
+// Several rules can also be given at once:
+rule zero × $y ↪ zero
+with succ $x × $y ↪ $y + $x × $y;
+
+/* We now would like to prove some theorem about +. To this end, since
+Lambdapi does not come with a pre-defined logic, we first need to
+define what is a proposition and what is a proof.
+
+You usually just need to install a package defining some logics and
+require it in your development. For instance, using Opam, you can do:
+
+opam install lambdapi-logics
+
+Then, in your development, you can use one of the logics defined in
+this package (see https://github.com/Deducteam/lambdapi-logics for
+more details) as follows:
+
+require Logic.TFF.Main;
+
+This tells Lambdapi to load in the environment the symbols, rules,
+etc.  declared in the package Logic.TFF, which defines multi-sorted
+first-order logic. A symbol f of Logic.TFF can then be refered to by
+Logic.TFF.f.  To avoid writing Logic.TFF every time, you can do:
+
+open Logic.TFF.Main;
+
+The two operations can also be done at the same time by simply writing;
+
+require open Logic.TFF;
+
+But we are going to define our own logic hereafter to show that it is
+simple. */
+
+// We first declare a type for propositions:
+symbol Prop : TYPE;
+
+// and symbols for building propositions:
+symbol = : ℕ → ℕ → Prop;
+notation = infix 1;
+
+/* We then use the "proposition-as-type" technique to reduce
+proof-checking to type-checking. To this end, we define a type for the
+proofs of a proposition: */
+injective symbol Prf : Prop → TYPE;
+  /* Note that this is a type-level function, that is, a function that
+     takes as argument a term of type Prop and return a term of type TYPE.
+
+     Moreover, we declare Prf as injective. This means that Prf
+     should satisfy the following property:
+       if Prf(p) ≡ Prf(q) then p ≡ q.
+     The verification of this property is left to the user.
+     This information is used by Lambdapi to simplify a unification constraint
+     of the form Prf(p) ≡ Prf(q) into p ≡ q (see below). */
+
+/* We then say that a proof of a proposition "p" is any term of type
+"Prf(p)". We therefore need to declare axioms saying which
+propositions are true. For instance, a usual axiom for equality is
+that it is a reflexive relation: */
+symbol =-refl x : Prf(x = x);
+  /* For all x, "=-refl x" is a proof of the proposition "x = x".
+     Note that Lambdapi can infer the type of "x" automatically:
+     the user does not need to write "symbol =-refl (x : ℕ) : Prf(x = x)". */
+
+/* Another usual axiom is that function application preserves equality: */
+symbol =-succ x y : Prf(x = y) → Prf(succ x = succ y);
+
+/* We also need to declare that we can prove any proposition "p" on natural
+numbers by induction: */
+symbol ind_ℕ (p : ℕ → Prop)
+  (case-zero : Prf(p zero))
+  (case-succ : Π x : ℕ, Prf(p x) → Prf(p (succ x)))
+     /* While "A → B" is the Lambdapi type of functions from "A" to "B",
+        "Π x : A, B(x)" is the Lambdapi type of so-called "dependent" functions
+        since x may occur in B(x). This is the type of functions mapping
+        any element a of type A to some element of type B(a).
+        It boils down to "A → B" if x does not occur in B.
+        Hence, case-succ is a function that takes as arguments a natural
+        number x and a proof that "p x" is true, and returns a proof that
+        "p (succ x)" is true. */
+  (n : ℕ)
+  : Prf(p n);
+
+/* We will later see that this induction principle can in fact be
+automatically generated by Lambdapi by using the "inductive" command
+when declaring ℕ, zero and succ. */
+ 
+/* We are now ready to prove that, for any natural number "x",
+"zero + x" is equal to "x", that is, to show that there exists a term, that
+we will call "zero_is_neutral_for_+", of type "Π x : ℕ, Prf (zero + x = x)".
+To this end, Lambdapi provides an interactive mode (launched by the keyword
+"begin") to enable users to define this term step by step using tactics. */
+
+opaque /* We declare the symbol as opaque as we do not want Lambdapi
+to unfold it later. */
+symbol zero_is_neutral_for_+ x : Prf (zero + x = x) ≔
+
+begin
+/* Here, in Emacs or VSCode, the system prints the following goal to prove:
+?zero_is_neutral_for_+: Π x: ℕ, Prf ((zero + x) = x) */
+
+/* To proceed by induction on x, we simply need to say that
+?zero_is_neutral_for_+ should be of the form "ind_ℕ _ _ _"
+where "_" stands for a term to be built.
+This can be done by using the "refine" tactic: */
+
+/* However, if we simply write "refine ind_ℕ _ _ _",
+Lambdapi will complain with the following error message:
+"Missing subproofs (0 subproofs for 2 subgoals)."
+This is because we gave no subproof for the case-zero and case-succ arguments.
+Indeed, in Lambdapi, proofs must be well structured, that is, a tactic
+must be followed by as many subproofs enclosed between curly brackets
+as the number of subgoals generated by the tactic. So, here, we need to write
+"refine nat _ _ _ {} {}" and then write the missing subproofs. */
+
+/* Remark: if we hadn't declared Prf as injective, we would have gotten
+  4 subgoals. the first generated subgoal would not have been a typing goal
+  but the following unification goal:
+  "Prf (?4 n) ≡ Prf ((zero + n) = n)"
+  where "?4" stands for the unknown predicate "p" that we try to prove,
+  which would have been the second goal, the third goal being the case for
+  zero, and the fourth goal being the case for succ.
+  This is one of the interesting features of Lambdapi to have unification
+  goals. However, currently, Lambdapi has only one tactic for unification
+  goals, namely "solve", which is applied automatically and thus didn't work
+  here. However, we can see that, to simplify this unification goal to
+  "?4 n ≡ (zero + n) = n"
+  we need Prf to be injective. */
+
+refine ind_ℕ _ _ _
+  { /* Here comes the proof of the first generated subgoal:
+    "Prf ((zero + zero) = zero)".
+
+    Note that Lambdapi infered the predicate to prove automatically.
+
+    To prove the first subgoal, we can first ask Lambdapi to simplify it
+    by applying user-defined rewriting rules with the tactic "simplify": */
+    simplify;
+
+    /* We then get the following goal:
+    "Prf (zero = zero)"
+    which can be solved by using =-refl: */
+    refine =-refl zero;
+  }
+  { /* Here comes the proof of the second generated subgoal:
+    "Π x: ℕ, Prf ((zero + x) = x) → Prf ((zero + succ x) = succ x)"
+
+    We start by assuming a given x : ℕ such that "zero + x = x"
+    using the tactic "assume": */
+    assume x hyp_on_x;
+    /* Again, we can simplify the goal: */
+    simplify;
+    /* We can then conclude by using the axiom =-succ and the assumption
+    hyp_on_x: */
+    refine =-succ (zero + x) x hyp_on_x;
+    /* Alternatively, we could use the "rewrite" tactic of Lambdapi,
+    to replace "zero + x" by "x", but this requires to set up a number
+    of "builtins" (see below). */
+  };
+end;
+
+/* Remark: now that we proved that "zero + x" is equal to "x", we can turn
+this equality into a rewrite rule to reason modulo this rule automatically. */
+rule zero + $y ↪ $y;
+
+/* We are going to see below how this first proof can be simplified
+by using more advanced features of Lambdapi. */
+
+/* First, the induction principle on natural numbers can be automatically
+generated by Lambdapi by using the command "inductive",
+as long as the builtins "Prop" and "P" are set: */
+builtin "Prop" ≔ Prop;
+builtin "P" ≔ Prf;
+inductive Nat : TYPE ≔ z : Nat | s : Nat → Nat;
+
+/* To see what has been generated, you can write: */
+print Nat;
+/* prints:
+
+constant symbol Nat: TYPE 
+
+constructors:
+  z: Nat
+  s: Nat → Nat
+
+induction principle:
+  ind_Nat: Π p0: (Nat → Prop), P (p0 z) → (Π x0: Nat, P (p0 x0) → P (p0 (s x0))) → Π x0: Nat, P (p0 x0)
+*/
+print ind_Nat;
+/* prints:
+
+symbol ind_Nat
+: Π p0: (Nat → Prop), P (p0 z) → (Π x0: Nat, P (p0 x0) → P (p0 (s x0))) → Π x0: Nat, P (p0 x0)
+
+rules:
+  ind_Nat $v0_p0 $v1_z $v2_s z ↪ $v1_z
+  ind_Nat $v0_p0 $v1_z $v2_s (s $v3_x0) ↪ $v2_s $v3_x0 (ind_Nat $v0_p0 $v1_z $v2_s $v3_x0)
+*/
+print one; // to see the definition of ten
+print +; // to see the type, notation and rules of +
+
+/* It is also possible now to replace the tactic "refine ind_Nat _ _ _"
+by a call to the tactic "induction" (see below). */
+
+/* Similarly, we can define a type for lists of natural numbers: */
+inductive List_Nat : TYPE ≔
+| nil_Nat : List_Nat
+| cons_Nat : Nat → List_Nat → List_Nat;
+
+/* But what if we want to have lists of booleans, or lists of lists of
+natural numbers, etc.? Lambdapi does not allow to quantify over
+types. On the other hand, it is possible to interpret objects as types
+using type-level rewriting rules, in the same way the function Prf
+maps terms of type Prop to types. We can define polymorphic objects by
+defining a type for type codes, and quantify over type codes instead
+of types: */
+
+symbol Set : TYPE; // type for type codes
+injective symbol τ : Set → TYPE; // function interpreting type codes as types
+
+// For instance, we can define a code for Nat:
+symbol nat : Set;
+rule τ nat ↪ Nat;
+
+// We can now define polymorphic lists:
+
+(a:Set) inductive 𝕃:TYPE ≔
+| □ /* \Box */ : 𝕃 a
+| ⸬ /* :: */ : τ a → 𝕃 a → 𝕃 a;
+
+/* We are now going to see how to use tactics related to equality like
+"reflexivity", "symmetry" and "rewrite". To this end, we need to use a
+polymorphic equality and define a few more builtins that are necessary
+for Lambdapi to generate the corresponding proofs. */
+
+constant // means that we cannot add rules later
+symbol ≃ [a] /* arguments between square brackets are implicit
+and must not be written later, unless they are enclosed between square brackets
+or if the symbol is prefixed by "@". */ 
+: τ a → τ a → Prop;
+
+notation ≃ infix 1;
+
+constant symbol ≃-refl [a] (x:τ a) : Prf(x ≃ x);
+constant symbol ≃-ind [a] [x y:τ a] : Prf(x ≃ y) → Π p, Prf(p y) → Prf(p x);
+  // Leibniz principle.
+
+builtin "T" ≔ τ;
+builtin "eq" ≔ ≃;
+builtin "refl"  ≔ ≃-refl;
+builtin "eqind" ≔ ≃-ind;
+
+/* We now reprove our theorem on the inductive type Nat instead of ℕ,
+using the tactics "induction", "reflexivity" and "rewrite".
+To this end, we first need to define addition on Nat: */
+
+symbol ⊕ : Nat → Nat → Nat;
+notation ⊕ infix right 10;
+rule $x ⊕ z ↪ $x
+with $x ⊕ s $y ↪ s ($x ⊕ $y);
+
+opaque symbol zero_is_neutral_for_⊕ x : Prf(z ⊕ x ≃ x) ≔
+begin
+induction
+  { simplify; reflexivity; }
+  { assume x hyp_on_x; simplify; rewrite hyp_on_x; reflexivity; }
+end;
+
+/* Note finally that a development can be split into several
+files. For instance, imagine that your development is made of file1.lp
+and file2.lp, and that file2.lp uses symbols defined in
+file1.lp. Then, you should create a file lambdapi.pkg with the
+following two lines:
+
+package_name = my_package
+root_path = my_package
+
+where my_package is the name of your package. Then, at the beginning
+of file2.lp, you should add:
+
+require my_package.file1;
+*/
diff --git a/vendor/README.md b/vendor/README.md
index a0ceb6b4e5..77a953e64c 100644
--- a/vendor/README.md
+++ b/vendor/README.md
@@ -331,6 +331,7 @@ This is a list of grammars that Linguist selects to provide syntax highlighting
 - **LSL:** [textmate/secondlife-lsl.tmbundle](https://github.com/textmate/secondlife-lsl.tmbundle)
 - **LTspice Symbol:** [Alhadis/language-pcb](https://github.com/Alhadis/language-pcb)
 - **LabVIEW:** [textmate/xml.tmbundle](https://github.com/textmate/xml.tmbundle)
+- **Lambdapi:** [Deducteam/sublime-lambdapi](https://github.com/Deducteam/sublime-lambdapi)
 - **Lark:** [Alhadis/language-grammars](https://github.com/Alhadis/language-grammars)
 - **Lasso:** [bfad/Sublime-Lasso](https://github.com/bfad/Sublime-Lasso)
 - **Latte:** [textmate/php-smarty.tmbundle](https://github.com/textmate/php-smarty.tmbundle)
diff --git a/vendor/grammars/sublime-lambdapi b/vendor/grammars/sublime-lambdapi
new file mode 160000
index 0000000000..3f6ecece6c
--- /dev/null
+++ b/vendor/grammars/sublime-lambdapi
@@ -0,0 +1 @@
+Subproject commit 3f6ecece6c9fdc39133804cb31f7e6f20b64ff8a
diff --git a/vendor/licenses/git_submodule/sublime-lambdapi.dep.yml b/vendor/licenses/git_submodule/sublime-lambdapi.dep.yml
new file mode 100644
index 0000000000..b374aab2e4
--- /dev/null
+++ b/vendor/licenses/git_submodule/sublime-lambdapi.dep.yml
@@ -0,0 +1,31 @@
+---
+name: sublime-lambdapi
+version: 3f6ecece6c9fdc39133804cb31f7e6f20b64ff8a
+type: git_submodule
+homepage: https://github.com/Deducteam/sublime-lambdapi.git
+license: mit
+licenses:
+- sources: LICENSE
+  text: |-
+    The MIT License (MIT)
+
+    Copyright (c) 2014 Inria
+
+    Permission is hereby granted, free of charge, to any person obtaining a copy
+    of this software and associated documentation files (the "Software"), to deal
+    in the Software without restriction, including without limitation the rights
+    to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+    copies of the Software, and to permit persons to whom the Software is
+    furnished to do so, subject to the following conditions:
+
+    The above copyright notice and this permission notice shall be included in all
+    copies or substantial portions of the Software.
+
+    THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+    IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+    FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+    AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+    LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+    OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+    SOFTWARE.
+notices: []