X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fmodels%2Flist_support.ma;h=ea701bb9db69cba6b1efa532efc6b01123fef0d8;hb=b12a46d53cf80d40b253ca5dd495397c5c0b4287;hp=4a335e01edeb8b941dc749250ba16e3880763861;hpb=8d367045e504f594c280d2c87f906695ef9671ee;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/models/list_support.ma b/helm/software/matita/contribs/dama/dama/models/list_support.ma
index 4a335e01e..ea701bb9d 100644
--- a/helm/software/matita/contribs/dama/dama/models/list_support.ma
+++ b/helm/software/matita/contribs/dama/dama/models/list_support.ma
@@ -171,7 +171,7 @@ intros 2; elim n;
         |1: rewrite < H2; rewrite > len_append; rewrite > plus_n_SO; reflexivity]]]
 qed.
 
-include "cprop_connectives.ma".
+include "logic/cprop_connectives.ma".
 
 definition eject_N ≝
   λP.λp:∃x:nat.P x.match p with [ex_introT p _ ⇒ p].