...

[helm.git] / helm / software / matita / contribs / dama / dama / models / list_support.ma

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 4a335e01edeb8b941dc749250ba16e3880763861..ea701bb9db69cba6b1efa532efc6b01123fef0d8 100644 (file)
--- 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].