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 "basic_2/substitution/lsuby.ma".
17 (* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED SUBSTITUTION *******************)
19 (* Main properties **********************************************************)
21 theorem lsuby_trans: ∀l,m. Transitive … (lsuby l m).
22 #l #m #L1 #L2 #H elim H -L1 -L2 -l -m
23 [ #L1 #l #m #X #H lapply (lsuby_inv_atom1 … H) -H
25 | #I1 #I2 #L1 #L #V1 #V #_ #IHL1 #X #H elim (lsuby_inv_zero1 … H) -H //
26 * #I2 #L2 #V2 #HL2 #H destruct /3 width=1 by lsuby_zero/
27 | #I1 #I2 #L1 #L2 #V #m #_ #IHL1 #X #H elim (lsuby_inv_pair1 … H) -H //
28 * #I2 #L2 #HL2 #H destruct /3 width=1 by lsuby_pair/
29 | #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #IHL1 #X #H elim (lsuby_inv_succ1 … H) -H //
30 * #I2 #L2 #V2 #HL2 #H destruct /3 width=1 by lsuby_succ/