#f #t #k #p * #q * #r #Hr #H1 #H2 destruct
@(ex2_intro โฆ (๐ฑkโ๐บโr))
/2 width=1 by in_comp_iref/
qed-.
lemma lift_term_iref_pap_dx (f) (t) (k:pnat):
#f #t #k #p * #q * #r #Hr #H1 #H2 destruct
@(ex2_intro โฆ (๐ฑkโ๐บโr))
/2 width=1 by in_comp_iref/
qed-.
lemma lift_term_iref_pap_dx (f) (t) (k:pnat):