...

[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 c8d2a9473f528e78e956f717f7650b984ee8ffe0..166ba5d7e3de10a6ad24a2525f259de44a1ccf1a 100644 (file)
--- a/matita/matita/lib/basics/star.ma
+++ b/matita/matita/lib/basics/star.ma
@@ -46,8 +46,8 @@ qed.
   
 (* star *)
 inductive star (A:Type[0]) (R:relation A) (a:A): A → Prop ≝
-  |inj: ∀b,c.star A R a b → R b c → star A R a c
-  |refl: star A R a a.
+  |sstep: ∀b,c.star A R a b → R b c → star A R a c
+  |srefl: star A R a a.
 
 lemma R_to_star: ∀A,R,a,b. R a b → star A R a b.
 #A #R #a #b /2/
@@ -93,22 +93,22 @@ qed.
 
 (* right associative version of star *)
 inductive starl (A:Type[0]) (R:relation A) : A → A → Prop ≝
-  |injl: ∀a,b,c.R a b → starl A R b c → starl A R a c
+  |sstepl: ∀a,b,c.R a b → starl A R b c → starl A R a c
   |refll: ∀a.starl A R a a.
  
 lemma starl_comp : ∀A,R,a,b,c.
   starl A R a b → R b c → starl A R a c.
 #A #R #a #b #c #Hstar elim Hstar 
-  [#a1 #b1 #c1 #Rab #sbc #Hind #a1 @(injl … Rab) @Hind //
-  |#a1 #Rac @(injl … Rac) //
+  [#a1 #b1 #c1 #Rab #sbc #Hind #a1 @(sstepl … Rab) @Hind //
+  |#a1 #Rac @(sstepl … Rac) //
   ]
 qed.
 
 lemma star_compl : ∀A,R,a,b,c.
   R a b → star A R b c → star A R a c.
 #A #R #a #b #c #Rab #Hstar elim Hstar 
-  [#b1 #c1 #sbb1 #Rb1c1 #Hind @(inj … Rb1c1) @Hind
-  |@(inj … Rab) //
+  [#b1 #c1 #sbb1 #Rb1c1 #Hind @(sstep … Rb1c1) @Hind
+  |@(sstep … Rab) //
   ]
 qed.