- main lemmas about abstract reducibility candidates closed

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / reducibility / tpr_lift.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma
index 91da5fabe90b28ec8d64e72afdb19d43f040dbde..be40639a863d6f7fbe85cbe582ade28fd9f95bcc 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma
@@ -101,8 +101,8 @@ qed.
 
 (* Advanced inversion lemmas ************************************************)
 
-fact tpr_inv_abst1_aux: ∀U1,U2. U1 ➡ U2 → ∀V1,T1. U1 = 𝕔{Abst} V1. T1 →
-                        ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = 𝕔{Abst} V2. T2.
+fact tpr_inv_abst1_aux: ∀U1,U2. U1 ➡ U2 → ∀V1,T1. U1 = ⓛV1. T1 →
+                        ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓛV2. T2.
 #U1 #U2 * -U1 -U2
 [ #I #V #T #H destruct
 | #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
@@ -116,6 +116,6 @@ fact tpr_inv_abst1_aux: ∀U1,U2. U1 ➡ U2 → ∀V1,T1. U1 = 𝕔{Abst} V1. T1
 qed.
 
 (* Basic_1: was pr0_gen_abst *)
-lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ➡ U2 →
-                     ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = 𝕔{Abst} V2. T2.
+lemma tpr_inv_abst1: ∀V1,T1,U2. ⓛV1. T1 ➡ U2 →
+                     ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓛV2. T2.
 /2 width=3/ qed-.