- some confluence results for focalized reduction and computation

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / computation / lfprs_aaa.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_aaa.ma
index a1337787c04f9ee6a022f2d284b12aa0fa2f2697..5c6cd31cbaaf38e8afd0f08736abdee0fcf6a5fc 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_aaa.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_aaa.ma
@@ -23,9 +23,3 @@ lemma aaa_lfprs_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. ⦃L1⦄ ➡* ⦃L2
 #L1 #T #A #HT #L2 #HL12
 @(TC_Conf3 … (λL,A. L ⊢ T ⁝ A) … HT ? HL12) /2 width=3/
 qed.
-(*
-(* Note: this should be rephrased in terms of fprs *)
-lemma aaa_lfprs_cprs_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2. ⦃L1⦄ ➡* ⦃L2⦄ →
-                           ∀T2. L2 ⊢ T1 ➡* T2 → L2 ⊢ T2 ⁝ A.
-/3 width=3/ qed.
-*)