-lemma at_fwd_id: ∀f,p,i. @❪i, p⨮f❫ ≘ i → 𝟏 = p.
-#f #p #i #H elim (gr_pat_des_id … H) -H
-#g #H elim (push_inv_seq_dx … H) -H //
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma tr_pat_O1: ∀p,f. (p⨮f)@❨𝟏❩ = p.
-// qed.
-
-lemma tr_pat_S1: ∀p,f,i. (p⨮f)@❨↑i❩ = f@❨i❩+p.
-// qed.
-
-lemma tr_pat_eq_repl (i): gr_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
-#i elim i -i [2: #i #IH ] * #p1 #f1 * #p2 #f2 #H
-elim (eq_inv_seq_aux … H) -H #Hp #Hf //
->tr_pat_S1 >tr_pat_S1 /3 width=1 by eq_f2/
-qed.
-
-lemma tr_pat_S2: ∀f,i. (↑f)@❨i❩ = ↑(f@❨i❩).
-* #p #f * //
-qed.
-
-(* Main inversion lemmas ****************************************************)
-
-theorem tr_pat_inj: ∀f,i1,i2,j. f@❨i1❩ = j → f@❨i2❩ = j → i1 = i2.
-/2 width=4 by gr_pat_inj/ qed-.
-
-corec theorem nstream_eq_inv_ext: ∀f1,f2. (∀i. f1@❨i❩ = f2@❨i❩) → f1 ≗ f2.
-* #p1 #f1 * #p2 #f2 #Hf @stream_eq_cons
-[ @(Hf (𝟏))
-| @nstream_eq_inv_ext -nstream_eq_inv_ext #i
- ltr_pat (Hf (𝟏)) >tr_pat_O1 >tr_pat_O1 #H destruct
- ltr_pat (Hf (↑i)) >tr_pat_S1 >tr_pat_S1 #H
- /3 width=2 by eq_inv_pplus_bi_dx, eq_inv_psucc_bi/
-]
+(*** at_fwd_id *)
+lemma tr_pat_des_id (f):
+ ∀p,i. @⧣❨i, 𝐭❨p⨮f❩❩ ≘ i → 𝟏 = p.
+#f #p #i #H lapply (pr_pat_des_id … H) -H #H
+elim (eq_inv_pr_push_cons … H) -H //