diff --git a/TODO.md b/TODO.md
index 7d077b8..2ee189a 100644
--- a/TODO.md
+++ b/TODO.md
@@ -7,8 +7,6 @@ TODO
 
 - why the mapping of ITLIST does not work anymore ?
 
-- in lp output, replace T by ⊤ ?
-
 - write progress in an ocaml program, and estimate time wrt size of files
 
 - use a single term_abbrev file for each theorem, and split it
diff --git a/erasing.lp b/erasing.lp
index 55267b1..34e0043 100644
--- a/erasing.lp
+++ b/erasing.lp
@@ -29,17 +29,17 @@ builtin "ex_def" ≔ ∃_def;
 builtin "not" ≔ ¬;
 builtin "not_def" ≔ ¬_def;
 
-builtin "True" ≔ T;
-builtin "T_def" ≔ T_def;
+builtin "True" ≔ ⊤;
+builtin "T_def" ≔ ⊤_def;
 
-builtin "False" ≔ F;
-builtin "F_def" ≔ F_def;
+builtin "False" ≔ ⊥;
+builtin "F_def" ≔ ⊥_def;
 
 builtin "ex1" ≔ ∃₁;
 builtin "ex1_def" ≔ ∃₁_def;
 
 // natural deduction rules
-builtin "Logic.I" ≔ Tᵢ;
+builtin "Logic.I" ≔ ⊤ᵢ;
 builtin "conj" ≔ ∧ᵢ;
 builtin "proj1" ≔ ∧ₑ₁;
 builtin "proj2" ≔ ∧ₑ₂;
diff --git a/theory_hol.lp b/theory_hol.lp
index 2f3c76e..84a2a40 100644
--- a/theory_hol.lp
+++ b/theory_hol.lp
@@ -26,18 +26,18 @@ opaque symbol SYM [a] [x y : El a] (xy: Prf (= x y)) : Prf (= y x) ≔
 /* HOL-Light derived connectives */
 constant symbol ∃₁ [A] : El (fun (fun A bool) bool);
 constant symbol ¬ : El (fun bool bool);
-constant symbol F : El bool;
+constant symbol ⊥ : El bool;
 constant symbol ∨ : El (fun bool (fun bool bool));
 constant symbol ∃ [A] : El (fun (fun A bool) bool);
 constant symbol ∀ [A] : El (fun (fun A bool) bool);
 constant symbol ⇒ : El (fun bool (fun bool bool));
 constant symbol ∧ : El (fun bool (fun bool bool));
-constant symbol T : El bool;
+constant symbol ⊤ : El bool;
 
 /* Natural deduction rules */
 rule Prf (⇒ $p $q) ↪ Prf $p → Prf $q;
 rule Prf (∀ $p) ↪ Π x, Prf ($p x);
-symbol Tᵢ : Prf T;
+symbol ⊤ᵢ : Prf ⊤;
 symbol ∧ᵢ [p : El bool] : Prf p → Π [q : El bool], Prf q → Prf (∧ p q);
 symbol ∧ₑ₁ [p q : El bool] : Prf (∧ p q) → Prf p;
 symbol ∧ₑ₂ [p q : El bool] : Prf (∧ p q) → Prf q;
diff --git a/xlp.ml b/xlp.ml
index d6a8405..97c6e22 100644
--- a/xlp.ml
+++ b/xlp.ml
@@ -32,6 +32,8 @@ let name =
     | "==>" -> "⇒"
     | "!" -> "∀"
     | "?" -> "∃"
+    | "F" -> "⊥"
+    | "T" -> "⊤"
     | "?!" -> "∃₁"
     | "~" -> "¬"
     | "-->" -> "⟶" (* 27F6 *)
@@ -504,7 +506,7 @@ let proof tvs rmap =
       int oc (pos_first (fun th -> concl th = t) !the_axioms);
       list_prefix " " typ oc (type_vars_in_term t);
       list_prefix " " term oc (frees t)
-    | Ptruth -> string oc "Tᵢ"
+    | Ptruth -> string oc "⊤ᵢ"
     | Pconj(k1,k2) -> string oc "∧ᵢ "; sub_at oc k1; char oc ' '; sub_at oc k2
     | Pconjunct1 k -> string oc "∧ₑ₁ "; sub_at oc k
     | Pconjunct2 k -> string oc "∧ₑ₂ "; sub_at oc k