(* Properties with generic relocation ***************************************)
(* Basic_1: was just: sn3_lift *)
(* Basic_2A1: was just: csx_lift *)
(* Properties with generic relocation ***************************************)
(* Basic_1: was just: sn3_lift *)
(* Basic_2A1: was just: csx_lift *)
qed-.
(* Inversion lemmas with generic slicing ************************************)
(* Basic_1: was just: sn3_gen_lift *)
(* Basic_2A1: was just: csx_inv_lift *)
qed-.
(* Inversion lemmas with generic slicing ************************************)
(* Basic_1: was just: sn3_gen_lift *)
(* Basic_2A1: was just: csx_inv_lift *)
-lemma csx_inv_lifts: ∀h,o,G. d_deliftable1 … (csx h o G).
-#h #o #G #L #U #H @(csx_ind … H) -U
+lemma csx_inv_lifts (G):
+ d_deliftable1 … (csx G).
+#G #L #U #H @(csx_ind … H) -U