include "delayed_updating/substitution/fsubst.ma".
include "delayed_updating/substitution/lift_prototerm_eq.ma".
include "delayed_updating/substitution/fsubst.ma".
include "delayed_updating/substitution/lift_prototerm_eq.ma".
(* FOCALIZED SUBSTITUTION ***************************************************)
(* Constructions with lift for preterm **************************************)
lemma lift_term_fsubst_sn (f) (t) (u) (p):
(* FOCALIZED SUBSTITUTION ***************************************************)
(* Constructions with lift for preterm **************************************)
lemma lift_term_fsubst_sn (f) (t) (u) (p):