1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground/relocation/pr_sle.ma".
17 (* INCLUSION FOR PARTIAL RELOCATION MAPS ************************************)
19 (* Main constructions *******************************************************)
22 corec theorem pr_sle_trans:
25 #f1 #f #g1 #g #Hf #H1 #H #g2 #H0
26 [ cases (pr_sle_inv_push_sn … H0 … H) *
27 |*: cases (pr_sle_inv_next_sn … H0 … H)
29 /3 width=5 by pr_sle_push, pr_sle_next, pr_sle_weak/