include "delayed_updating/substitution/lift_prototerm_id.ma".
include "delayed_updating/substitution/lift_path_uni.ma".
include "delayed_updating/substitution/lift_prototerm_id.ma".
include "delayed_updating/substitution/lift_path_uni.ma".
lemma lift_iref_sn (f) (t:prototerm) (n:pnat):
(šfļ¼ ā§£āØnā©.ā[ā*[n]f]t) ā ā[f](šn.t).
#f #t #n #p * #q * #r #Hr #H1 #H2 destruct
lemma lift_iref_sn (f) (t:prototerm) (n:pnat):
(šfļ¼ ā§£āØnā©.ā[ā*[n]f]t) ā ā[f](šn.t).
#f #t #n #p * #q * #r #Hr #H1 #H2 destruct
ā[f](šn.t) ā šfļ¼ ā§£āØnā©.ā[ā*[n]f]t.
#f #t #n #p * #q #Hq #H0 destruct
elim (in_comp_inv_iref ā¦ Hq) -Hq #p #H0 #Hp destruct
ā[f](šn.t) ā šfļ¼ ā§£āØnā©.ā[ā*[n]f]t.
#f #t #n #p * #q #Hq #H0 destruct
elim (in_comp_inv_iref ā¦ Hq) -Hq #p #H0 #Hp destruct