+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "delayed_updating/unwind0/unwind1_path.ma".
+include "delayed_updating/notation/functions/black_downtriangle_2.ma".
+
+(* EXTENDED UNWIND FOR PATH *************************************************)
+
+definition unwind2_path (f) (p) ā
+ ā¼ā[f]p.
+
+interpretation
+ "extended unwind (path)"
+ 'BlackDownTriangle f p = (unwind2_path f p).
+
+(* Basic constructions ******************************************************)
+
+lemma unwind2_path_unfold (f) (p):
+ ā¼ā[f]p = ā¼[f]p.
+// qed.
+
+lemma unwind2_path_id (p):
+ ā¼p = ā¼[š¢]p.
+// qed.
+
+lemma unwind2_path_empty (f):
+ (š) = ā¼[f]š.
+// qed.
+
+lemma unwind2_path_d_empty (f) (n):
+ (š±(f@āØnā©)āš) = ā¼[f](š±nāš).
+// qed.
+
+lemma unwind2_path_d_lcons (f) (p) (l) (n:pnat):
+ ā¼[š®āØf@āØnā©ā©](lāp) = ā¼[f](š±nālāp).
+#f #p #l #n
+<unwind2_path_unfold in ā¢ (???%);
+<lift_path_d_sn <lift_path_id <unwind1_path_d_lcons //
+qed.
+
+lemma unwind2_path_m_sn (f) (p):
+ ā¼[f]p = ā¼[f](šŗāp).
+#f #p
+<unwind2_path_unfold in ā¢ (???%);
+<lift_path_m_sn //
+qed.
+
+lemma unwind2_path_L_sn (f) (p):
+ (šāā¼[ā«Æf]p) = ā¼[f](šāp).
+#f #p
+<unwind2_path_unfold in ā¢ (???%);
+<lift_path_L_sn //
+qed.
+
+lemma unwind2_path_A_sn (f) (p):
+ (šāā¼[f]p) = ā¼[f](šāp).
+#f #p
+<unwind2_path_unfold in ā¢ (???%);
+<lift_path_A_sn //
+qed.
+
+lemma unwind2_path_S_sn (f) (p):
+ (š¦āā¼[f]p) = ā¼[f](š¦āp).
+#f #p
+<unwind2_path_unfold in ā¢ (???%);
+<lift_path_S_sn //
+qed.
+
+(* Main constructions *******************************************************)
+
+theorem unwind2_path_after_id_sn (p) (f):
+ ā¼[f]p = ā¼ā¼[f]p.
+// qed.
+
+(* Constructions with stream_eq *********************************************)
+
+lemma unwind2_path_eq_repl (p):
+ stream_eq_repl ā¦ (Ī»f1,f2. ā¼[f1]p = ā¼[f2]p).
+#p #f1 #f2 #Hf
+<unwind2_path_unfold <unwind2_path_unfold
+<(lift_path_eq_repl ā¦ Hf) -Hf //
+qed.
+
+(* Advanced eliminations with path ******************************************)
+
+lemma path_ind_unwind2 (Q:predicate ā¦):
+ Q (š) ā
+ (ān. Q (š) ā Q (š±nāš)) ā
+ (ān,l,p. Q (lāp) ā Q (š±nālāp)) ā
+ (āp. Q p ā Q (šŗāp)) ā
+ (āp. Q p ā Q (šāp)) ā
+ (āp. Q p ā Q (šāp)) ā
+ (āp. Q p ā Q (š¦āp)) ā
+ āp. Q p.
+#Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #p
+elim p -p [| * [ #n * ] ]
+/2 width=1 by/
+qed-.