]
qed-.
+lemma sprec_inv_dx: ∀p,q. p ≺ q → ∀q0. dx::q0 = q →
+ ◊ = p ∨ ∃∃p0. p0 ≺ q0 & dx::p0 = p.
+#p #q * -p -q
+[ #o #q #q0 #H destruct /2 width=1/
+| #p #q #q0 #H destruct
+| #p #q #q0 #H destruct
+| #o #p #q #Hpq #q0 #H destruct /3 width=3/
+| #q0 #H destruct
+]
+qed-.
+
lemma sprec_inv_rc: ∀p,q. p ≺ q → ∀p0. rc::p0 = p →
(∃∃q0. p0 ≺ q0 & rc::q0 = q) ∨
∃q0. sn::q0 = q.
| #o #p #q #_ #IHpq * #H destruct /3 width=1/
]
qed-.
+
+lemma sprec_fwd_in_inner: ∀p,q. p ≺ q → in_inner p → in_inner q.
+/3 width=3 by sprec_fwd_in_whd/
+qed-.