some work on extended reduction ...

[helm.git] / matita / matita / lib / basics / star.ma

diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma
index 36aee8fe45465c016a6ca3709046a0c6fefd11c7..f935f007058e32bf9f852fbcd03d7136658a5393 100644 (file)
--- a/matita/matita/lib/basics/star.ma
+++ b/matita/matita/lib/basics/star.ma
@@ -142,7 +142,7 @@ lemma star_ind_l: ∀A,R,a2. ∀P:predicate A.
 @(star_ind_l_aux … H1 H2 … Ha12) //
 qed.
 
-(* RC and star *)
+(* TC and star *)
 
 lemma TC_to_star: ∀A,R,a,b.TC A R a b → star A R a b.
 #R #A #a #b #TCH (elim TCH) /2/