(* Constructions with constructors ******************************************)
lemma unwind2_term_iref_sn (f) (t) (n:pnat):
- â\96¼[fâ\88\98ð\9d\90®â\9d¨nâ\9d©]t â\8a\86 â\96¼[f](ð\9d\9b\97n.t).
+ â\96¼[fâ\88\98ð\9d\90®â\9d¨nâ\9d©]t â\8a\86 â\96¼[f](ð\9d\9b\95n.t).
#f #t #n #p * #q #Hq #H0 destruct
@(ex2_intro … (𝗱n◗𝗺◗q))
/2 width=1 by in_comp_iref/
qed-.
lemma unwind2_term_iref_dx (f) (t) (n:pnat):
- â\96¼[f](ð\9d\9b\97n.t) ⊆ ▼[f∘𝐮❨n❩]t.
+ â\96¼[f](ð\9d\9b\95n.t) ⊆ ▼[f∘𝐮❨n❩]t.
#f #t #n #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):
- â\96¼[fâ\88\98ð\9d\90®â\9d¨nâ\9d©]t â\87\94 â\96¼[f](ð\9d\9b\97n.t).
+ â\96¼[fâ\88\98ð\9d\90®â\9d¨nâ\9d©]t â\87\94 â\96¼[f](ð\9d\9b\95n.t).
/3 width=2 by conj, unwind2_term_iref_sn, unwind2_term_iref_dx/
qed.