- the definition of the framework for strong normalization continues ...

[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 98a8caa509a45a343446a54f623385c771845d61..0f6196e523c40f6fca0f457f8ae0a2a94ca9b832 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma
@@ -107,6 +107,15 @@ lemma tpss_inv_sort1: ∀L,T2,k,d,e. L ⊢ ⋆k [d, e] ≫* T2 → T2 = ⋆k.
 ]
 qed-.
 
+(* Note: this can be derived from tpss_inv_atom1 *)
+lemma tpss_inv_gref1: ∀L,T2,p,d,e. L ⊢ §p [d, e] ≫* T2 → T2 = §p.
+#L #T2 #p #d #e #H @(tpss_ind … H) -T2
+[ //
+| #T #T2 #_ #HT2 #IHT destruct
+  >(tps_inv_gref1 … HT2) -HT2 //
+]
+qed-.
+
 lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫* U2 →
                       ∃∃V2,T2. L ⊢ V1 [d, e] ≫* V2 & 
                                L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ≫* T2 &