(**************************************************************************)
include "delayed_updating/unwind/unwind2_prototerm_eq.ma".
+include "delayed_updating/unwind/unwind2_path_append.ma".
include "delayed_updating/syntax/prototerm_constructors.ma".
-(* UNWIND FOR PROTOTERM *****************************************************)
+(* TAILED UNWIND FOR PROTOTERM **********************************************)
(* Constructions with constructors ******************************************)
-lemma unwind2_term_iref_sn (f) (t) (n:pnat):
- ▼[f∘𝐮❨n❩]t ⊆ ▼[f](𝛗n.t).
-#f #t #n #p * #q #Hq #H0 destruct
-@(ex2_intro … (𝗱n◗𝗺◗q))
+lemma unwind2_term_iref_sn (f) (t) (k:pnat):
+ ▼[f∘𝐮❨k❩]t ⊆ ▼[f](𝛕k.t).
+#f #t #k #p * #q #Hq #H0 destruct
+@(ex2_intro … (𝗱k◗𝗺◗q))
/2 width=1 by in_comp_iref/
qed-.
-lemma unwind2_term_iref_dx (f) (t) (n:pnat):
- â\96¼[f](ð\9d\9b\97n.t) â\8a\86 â\96¼[fâ\88\98ð\9d\90®â\9d¨n❩]t.
-#f #t #n #p * #q #Hq #H0 destruct
+lemma unwind2_term_iref_dx (f) (t) (k:pnat):
+ â\96¼[f](ð\9d\9b\95k.t) â\8a\86 â\96¼[fâ\88\98ð\9d\90®â\9d¨k❩]t.
+#f #t #k #p * #q #Hq #H0 destruct
elim (in_comp_inv_iref … Hq) -Hq #p #Hp #Ht destruct
/2 width=1 by in_comp_unwind2_path_term/
qed-.
-lemma unwind2_term_iref (f) (t) (n:pnat):
- ▼[f∘𝐮❨n❩]t ⇔ ▼[f](𝛗n.t).
+lemma unwind2_term_iref (f) (t) (k:pnat):
+ ▼[f∘𝐮❨k❩]t ⇔ ▼[f](𝛕k.t).
/3 width=2 by conj, unwind2_term_iref_sn, unwind2_term_iref_dx/
qed.