-lemma push_inv_seq_sn: ∀f,g,p. p⨮g = ⫯f → ∧∧ 𝟏 = p & g = f.
-#f #g #p <gr_push_unfold #H destruct /2 width=1 by conj/
-qed-.
-
-lemma push_inv_seq_dx: ∀f,g,p. ⫯f = p⨮g → ∧∧ 𝟏 = p & g = f.
-#f #g #p <gr_push_unfold #H destruct /2 width=1 by conj/
-qed-.
-
-lemma next_inv_seq_sn: ∀f,g,p. p⨮g = ↑f → ∃∃q. q⨮g = f & ↑q = p.
-* #q #f #g #p <gr_next_unfold #H destruct /2 width=3 by ex2_intro/
-qed-.
-
-lemma next_inv_seq_dx: ∀f,g,p. ↑f = p⨮g → ∃∃q. q⨮g = f & ↑q = p.
-* #q #f #g #p <gr_next_unfold #H destruct /2 width=3 by ex2_intro/
-qed-.
-