support for candidates of reducibility started ...

[helm.git] / matita / matita / contribs / lambda_delta / Ground_2 / star.ma

diff --git a/matita/matita/contribs/lambda_delta/Ground_2/star.ma b/matita/matita/contribs/lambda_delta/Ground_2/star.ma
index e438b44f0c6bea578f1b243f7985aa68a8f51ec6..097151367c0686266bf03fe3c637c999ec1b13b4 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Ground_2/star.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/star.ma
@@ -17,6 +17,8 @@ include "Ground_2/xoa_props.ma".
 
 (* PROPERTIES of RELATIONS **************************************************)
 
+definition predicate: Type[0] → Type[0] ≝ λA. A → Prop.
+
 definition Decidable: Prop → Prop ≝
    λR. R ∨ (R → False). 
 
@@ -105,16 +107,16 @@ qed.
 lemma TC_reflexive: ∀A,R. reflexive A R → reflexive A (TC … R).
 /2/ qed.
 
-lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:A→Prop.
+lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:predicate A.
                    P a1 → (∀a,a2. TC … R a1 a → R a a2 → P a → P a2) →
                    ∀a2. TC … R a1 a2 → P a2.
 #A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -Ha12 a2 /3/
 qed.
 
-definition NF: ∀A. relation A → relation A → A → Prop ≝
+definition NF: ∀A. relation A → relation A → predicate A ≝
    λA,R,S,a1. ∀a2. R a1 a2 → S a1 a2.
 
-inductive SN (A) (R,S:relation A): A → Prop ≝
+inductive SN (A) (R,S:relation A): predicate A ≝
 | SN_intro: ∀a1. (∀a2. R a1 a2 → (S a1 a2 → False) → SN A R S a2) → SN A R S a1
 .