initial properies of the "same top term constructor" predicate

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / computation / csn_cr.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma
index 5dadd06deed5da57084a7397f05ae6afc443bfaf..e71d2bd3e694e178da1a76e489579bd3d8dff816 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma
@@ -13,10 +13,27 @@
 (**************************************************************************)
 
 include "Basic_2/computation/acp_cr.ma".
-include "Basic_2/computation/csn.ma".
+include "Basic_2/computation/csn_lcpr.ma".
+include "Basic_2/computation/csn_vector.ma".
 
 (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
 
 (* Advanced properties ******************************************************)
+(*
+lemma csn_applv_theta: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
+                       ∀V,T. L ⊢ ⬇* ⓓV. ⒶV2s. T → L ⊢ ⬇* V → L ⊢ ⬇* ⒶV1s. ⓓV. T.
+#L #V1s #V2s * -V1s -V2s /2 width=1/
+#V1s #V2s #V1 #V2 #HV12 * -V1s -V2s /2 width=3/
+#V1s #V2s #W1 #W2 #HW12 #HV12s #V #T #H #HV
+lapply (csn_appl_theta … HV12 … H) -H -HV12 #H
+lapply (csn_fwd_pair_sn … H) #HV1
+@csn_appl_simple // #X #H1 #H2
+whd in ⊢ (? ? %);
+*)
+(*
+lemma csn_S5: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
+              ∀V,T. L. ⓓV ⊢ ⬇* ⒶV2s. T → L ⊢ ⬇* V → L ⊢ ⬇* ⒶV1s. ⓓV. T.
+#L #V1s #V2s #H elim H -V1s -V2s /2 width=1/
+*)
 
-axiom csn_acr: acr cpr (eq â\80¦) (csn â\80¦) (λL,T. L â\8a¢ â\87\93 T).
+axiom csn_acr: acr cpr (eq â\80¦) (csn â\80¦) (λL,T. L â\8a¢ â¬\87* T).