partial commit in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / unwind / unwind2_path_eq.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_eq.ma
index ed75b0d7a7d72e89097d3248b0994a923953e79d..c1b188b60041c9132cc9d3b66979acb05f12157e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_eq.ma
@@ -14,26 +14,16 @@
 
 include "delayed_updating/unwind/unwind2_path.ma".
 include "delayed_updating/unwind/unwind2_rmap_eq.ma".
-include "delayed_updating/unwind/unwind_gen_eq.ma".
-include "ground/relocation/tr_compose_compose.ma".
 
-(* UNWIND FOR PATH **********************************************************)
+(* TAILED UNWIND FOR PATH ***************************************************)
 
-(* Constructions with stream_eq *********************************************)
+(* Constructions with tr_map_eq *********************************************)
 
 lemma unwind2_path_eq_repl (p):
       stream_eq_repl … (λf1,f2. ▼[f1]p = ▼[f2]p).
-/3 width=1 by unwind2_rmap_eq_repl, unwind_gen_eq_repl/
+* // * [ #k ] #p #f1 #f2 #Hf //
+<unwind2_path_d_dx <unwind2_path_d_dx
+lapply (unwind2_rmap_eq_repl … Hf) -Hf
+[| #Hf <(tr_pap_eq_repl … Hf) -f2 ] //
 qed-.
 
-(* Properties with tr_compose ***********************************************)
-
-lemma unwind2_path_after (p) (f1) (f2):
-      ▼[f2]▼[f1]p = ▼[f2∘f1]p.
-#p @(path_ind_unwind … p) -p // [ #n #l #p | #p ] #IH #f1 #f2
-[ <unwind2_path_d_lcons <unwind2_path_d_lcons
-  >(unwind2_path_eq_repl … (tr_compose_assoc …)) //
-| <(unwind2_path_L_sn … f1) <unwind2_path_L_sn <unwind2_path_L_sn
-  >tr_compose_push_bi //
-]
-qed.