partial commit in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / etc / unwind2 / unwind_etc.etc

include "delayed_updating/unwind2/unwind_depth.ma".
include "ground/relocation/tr_uni_compose.ma".

lemma pippo (q) (p): 
      ▼[p]𝐢 ≗ ⇂*[↑❘q❘]▼[p●𝗟◗q]𝐢.
#q @(list_ind_rcons … q) -q //
#q * [ #n ] #IH #p //
<depth_d_dx >list_cons_shift <list_append_assoc
<unwind_rmap_d_dx
check tr_tls_compose_uni_sn