]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma
- renaming completed!
[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / computation / csn_vector.ma
index bddaaa89de3028d51c17d46f3910054d6a18c488..b4a087a1a7672141360864248d609e9f9f68efec 100644 (file)
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic_2/grammar/term_vector.ma".
-include "Basic_2/computation/csn.ma".
+include "basic_2/grammar/term_vector.ma".
+include "basic_2/computation/csn.ma".
 
 (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************)
 
@@ -39,7 +39,7 @@ qed.
 lemma csnv_inv_cons: ∀L,T,Ts. L ⊢ ⬇* T :: Ts → L ⊢ ⬇* T ∧ L ⊢ ⬇* Ts.
 /2 width=3/ qed-.
 
-include "Basic_2/computation/csn_cpr.ma".
+include "basic_2/computation/csn_cpr.ma".
 
 lemma csn_fwd_applv: ∀L,T,Vs. L ⊢ ⬇* Ⓐ Vs. T → L ⊢ ⬇* Vs ∧ L ⊢ ⬇* T.
 #L #T #Vs elim Vs -Vs /2 width=1/