+include "ground/arith/nat_le_plus.ma".
+include "ground/relocation/pr_compose.ma".
+include "ground/relocation/pr_nat_uni.ma".
+include "ground/relocation/pr_isi_nat.ma".
+include "ground/relocation/pr_ist_ist.ma".
+include "ground/relocation/pr_after_uni.ma".
+include "ground/relocation/pr_after_nat.ma".
+include "ground/relocation/pr_after_ist.ma".