diff --git a/examples/lean/tc.lean b/examples/lean/tc.lean
index 829fc1976..cb3449b18 100644
--- a/examples/lean/tc.lean
+++ b/examples/lean/tc.lean
@@ -9,26 +9,27 @@ infix 50 ⊆ : subrelation
 -- We define it as the intersection of all transitive relations containing R
 definition tcls {A : TypeU} (R : A → A → Bool) (a b : A)
 := ∀ P, (reflexive P) → (transitive P) → (R ⊆ P) → P a b
+notation 65 _⁺ : tcls  -- use superscript + as notation for transitive closure
 
-theorem tcls_trans {A : TypeU} {R : A → A → Bool} {a b c : A} (H1 : tcls R a b) (H2 : tcls R b c) : tcls R a c
+theorem tcls_trans {A : TypeU} {R : A → A → Bool} {a b c : A} (Hab : R⁺ a b) (Hbc : R⁺ b c) : R⁺ a c
 := take P, assume Hrefl Htrans Hsub,
-     let Pab : P a b := H1 P Hrefl Htrans Hsub,
-         Pbc : P b c := H2 P Hrefl Htrans Hsub
+     let Pab : P a b := Hab P Hrefl Htrans Hsub,
+         Pbc : P b c := Hbc P Hrefl Htrans Hsub
      in Htrans a b c Pab Pbc
 
-theorem tcls_refl {A : TypeU} (R : A → A → Bool) : ∀ a, tcls R a a
+theorem tcls_refl {A : TypeU} (R : A → A → Bool) : ∀ a, R⁺ a a
 := take a P, assume Hrefl Htrans Hsub,
       Hrefl a
 
-theorem tcls_sub {A : TypeU} {R : A → A → Bool} {a b : A} (H : R a b) : tcls R a b
+theorem tcls_sub {A : TypeU} {R : A → A → Bool} {a b : A} (H : R a b) : R⁺ a b
 := take P, assume Hrefl Htrans Hsub,
       Hsub a b H
 
-theorem tcls_step {A : TypeU} {R : A → A → Bool} {a b c : A} (H1 : R a b) (H2 : tcls R b c) : tcls R a c
+theorem tcls_step {A : TypeU} {R : A → A → Bool} {a b c : A} (H1 : R a b) (H2 : R⁺ b c) : R⁺ a c
 := take P, assume Hrefl Htrans Hsub,
       Htrans a b c (Hsub a b H1) (H2 P Hrefl Htrans Hsub)
 
-theorem tcls_smallest {A : TypeU} {R : A → A → Bool} : ∀ P, (reflexive P) → (transitive P) → (R ⊆ P) → (tcls R ⊆ P)
+theorem tcls_smallest {A : TypeU} {R : A → A → Bool} : ∀ P, (reflexive P) → (transitive P) → (R ⊆ P) → (R⁺ ⊆ P)
 := take P, assume Hrefl Htrans Hsub,
-     take a b, assume H : tcls R a b,
+     take a b, assume H : R⁺ a b,
          have P a b : H P Hrefl Htrans Hsub