initial properies of the "same top term constructor" predicate

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

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma
index 2df67c9c226c7abfccbd81b1faef3f1ca0c0ae7a..043fa9a277e25087e892c2805158f7b480052a7d 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma
@@ -56,18 +56,13 @@ elim (term_eq_dec T1 T2) #HT12
 | -HT1 -HT2 /3 width=4/
 qed.
 
-axiom tpss_csn_trans: ∀L,T2. L ⊢ ⬇* T2 → ∀T1,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ ⬇* T1.
-(*
-#L #T2 #H @(csn_ind … H) -T2 #T2 #HT2 #IHT2 #T1 #d #e #HT12
-@csn_intro #T #HLT1 #HT1  
-*)
 (* Basic_1: was: sn3_cast *)
 lemma csn_cast: ∀L,W. L ⊢ ⬇* W → ∀T. L ⊢ ⬇* T → L ⊢ ⬇* ⓣW. T.
 #L #W #HW elim HW -W #W #_ #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT
 @csn_intro #X #H1 #H2
 elim (cpr_inv_cast1 … H1) -H1
 [ * #W0 #T0 #HLW0 #HLT0 #H destruct
-  elim (eq_false_inv_tpair … H2) -H2
+  elim (eq_false_inv_tpair_sn … H2) -H2
   [ /3 width=3/
   | -HLW0 * #H destruct /3 width=1/ 
   ]
@@ -77,19 +72,14 @@ qed.
 
 (* Basic forward lemmas *****************************************************)
 
-fact csn_fwd_flat2_aux: ∀L,U. L ⊢ ⬇* U → ∀I,V,T. U = ⓕ{I} V. T → L ⊢ ⬇* T.
+fact csn_fwd_flat_dx_aux: ∀L,U. L ⊢ ⬇* U → ∀I,V,T. U = ⓕ{I} V. T → L ⊢ ⬇* T.
 #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
 @csn_intro #T2 #HLT2 #HT2
 @(IH (ⓕ{I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/
 qed.
 
 (* Basic_1: was: sn3_gen_flat *)
-lemma csn_fwd_flat2: ∀I,L,V,T. L ⊢ ⬇* ⓕ{I} V. T → L ⊢ ⬇* T.
+lemma csn_fwd_flat_dx: ∀I,L,V,T. L ⊢ ⬇* ⓕ{I} V. T → L ⊢ ⬇* T.
 /2 width=5/ qed-.
 
-(*
-sn3/fwd sn3_gen_bind
-sn3/fwd sn3_gen_head
-*)
-
 (* Basic_1: removed theorems 3: sn3_gen_cflat sn3_cflat sn3_bind *)