// qed.
(* Basic inversions *********************************************************)
lemma prelift_label_inv_d_sn (f) (l) (k1):
// qed.
(* Basic inversions *********************************************************)
lemma prelift_label_inv_d_sn (f) (l) (k1):