support for candidates of reducibility started ...

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / unfold / tpss.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma
index 62eb25d49460d3390da3b14f1005ae7ba5a1d4b1..f21f3603eb01e5a35bd6d93460b2374f746bc7eb 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma
@@ -24,7 +24,7 @@ interpretation "partial unfold (term)"
 
 (* Basic eliminators ********************************************************)
 
-lemma tpss_ind: ∀d,e,L,T1. ∀R: term → Prop. R T1 →
+lemma tpss_ind: ∀d,e,L,T1. ∀R:predicate term. R T1 →
                 (∀T,T2. L ⊢ T1 [d, e] ≫* T → L ⊢ T [d, e] ≫ T2 → R T → R T2) →
                 ∀T2. L ⊢ T1 [d, e] ≫* T2 → R T2.
 #d #e #L #T1 #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) //